Theorem indispcon 27257

Description: The indiscrete topology (or trivial topology) on any set is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015.) (Revised by Mario Carneiro, 14-Aug-2015.)

Assertion

Ref	Expression
indispcon	|- { (/) , A } e. PCon

Proof of Theorem indispcon

Dummy variables x f y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		indistop 18722	. 2 |- { (/) , A } e. Top
2		simpl 457	. . . . . . . . . 10 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> x e. U. { (/) , A } )
3		0ex 4520	. . . . . . . . . . . 12 |- (/) e. _V
4		n0i 3740	. . . . . . . . . . . . . 14 |- ( x e. U. { (/) , A } -> -. U. { (/) , A } = (/) )
5		prprc2 4084	. . . . . . . . . . . . . . . 16 |- ( -. A e. _V -> { (/) , A } = { (/) } )
6	5	unieqd 4199	. . . . . . . . . . . . . . 15 |- ( -. A e. _V -> U. { (/) , A } = U. { (/) } )
7	3	unisn 4204	. . . . . . . . . . . . . . 15 |- U. { (/) } = (/)
8	6, 7	syl6eq 2508	. . . . . . . . . . . . . 14 |- ( -. A e. _V -> U. { (/) , A } = (/) )
9	4, 8	nsyl2 127	. . . . . . . . . . . . 13 |- ( x e. U. { (/) , A } -> A e. _V )
10	9	adantr 465	. . . . . . . . . . . 12 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> A e. _V )
11		uniprg 4203	. . . . . . . . . . . 12 |- ( ( (/) e. _V /\ A e. _V ) -> U. { (/) , A } = ( (/) u. A ) )
12	3, 10, 11	sylancr 663	. . . . . . . . . . 11 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> U. { (/) , A } = ( (/) u. A ) )
13		uncom 3598	. . . . . . . . . . . 12 |- ( (/) u. A ) = ( A u. (/) )
14		un0 3760	. . . . . . . . . . . 12 |- ( A u. (/) ) = A
15	13, 14	eqtri 2480	. . . . . . . . . . 11 |- ( (/) u. A ) = A
16	12, 15	syl6eq 2508	. . . . . . . . . 10 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> U. { (/) , A } = A )
17	2, 16	eleqtrd 2541	. . . . . . . . 9 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> x e. A )
18		simpr 461	. . . . . . . . . 10 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> y e. U. { (/) , A } )
19	18, 16	eleqtrd 2541	. . . . . . . . 9 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> y e. A )
20		ifcl 3929	. . . . . . . . 9 |- ( ( x e. A /\ y e. A ) -> if ( z = 0 , x , y ) e. A )
21	17, 19, 20	syl2anc 661	. . . . . . . 8 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> if ( z = 0 , x , y ) e. A )
22	21	adantr 465	. . . . . . 7 |- ( ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) /\ z e. ( 0 [,] 1 ) ) -> if ( z = 0 , x , y ) e. A )
23		eqid 2451	. . . . . . 7 |- ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) = ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) )
24	22, 23	fmptd 5966	. . . . . 6 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) : ( 0 [,] 1 ) --> A )
25		ovex 6215	. . . . . . 7 |- ( 0 [,] 1 ) e. _V
26		elmapg 7327	. . . . . . 7 |- ( ( A e. _V /\ ( 0 [,] 1 ) e. _V ) -> ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) e. ( A ^m ( 0 [,] 1 ) ) <-> ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) : ( 0 [,] 1 ) --> A ) )
27	10, 25, 26	sylancl 662	. . . . . 6 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) e. ( A ^m ( 0 [,] 1 ) ) <-> ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) : ( 0 [,] 1 ) --> A ) )
28	24, 27	mpbird 232	. . . . 5 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) e. ( A ^m ( 0 [,] 1 ) ) )
29		iitopon 20571	. . . . . 6 |- II e. (TopOn ` ( 0 [,] 1 ) )
30		cnindis 19012	. . . . . 6 |- ( ( II e. (TopOn ` ( 0 [,] 1 ) ) /\ A e. _V ) -> ( II Cn { (/) , A } ) = ( A ^m ( 0 [,] 1 ) ) )
31	29, 10, 30	sylancr 663	. . . . 5 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> ( II Cn { (/) , A } ) = ( A ^m ( 0 [,] 1 ) ) )
32	28, 31	eleqtrrd 2542	. . . 4 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) e. ( II Cn { (/) , A } ) )
33		0elunit 11504	. . . . 5 |- 0 e. ( 0 [,] 1 )
34		iftrue 3895	. . . . . 6 |- ( z = 0 -> if ( z = 0 , x , y ) = x )
35		vex 3071	. . . . . 6 |- x e. _V
36	34, 23, 35	fvmpt 5873	. . . . 5 |- ( 0 e. ( 0 [,] 1 ) -> ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) ` 0 ) = x )
37	33, 36	mp1i 12	. . . 4 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) ` 0 ) = x )
38		1elunit 11505	. . . . 5 |- 1 e. ( 0 [,] 1 )
39		ax-1ne0 9452	. . . . . . . 8 |- 1 =/= 0
40		neeq1 2729	. . . . . . . 8 |- ( z = 1 -> ( z =/= 0 <-> 1 =/= 0 ) )
41	39, 40	mpbiri 233	. . . . . . 7 |- ( z = 1 -> z =/= 0 )
42		ifnefalse 3899	. . . . . . 7 |- ( z =/= 0 -> if ( z = 0 , x , y ) = y )
43	41, 42	syl 16	. . . . . 6 |- ( z = 1 -> if ( z = 0 , x , y ) = y )
44		vex 3071	. . . . . 6 |- y e. _V
45	43, 23, 44	fvmpt 5873	. . . . 5 |- ( 1 e. ( 0 [,] 1 ) -> ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) ` 1 ) = y )
46	38, 45	mp1i 12	. . . 4 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) ` 1 ) = y )
47		fveq1 5788	. . . . . . 7 |- ( f = ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) -> ( f ` 0 ) = ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) ` 0 ) )
48	47	eqeq1d 2453	. . . . . 6 |- ( f = ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) -> ( ( f ` 0 ) = x <-> ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) ` 0 ) = x ) )
49		fveq1 5788	. . . . . . 7 |- ( f = ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) -> ( f ` 1 ) = ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) ` 1 ) )
50	49	eqeq1d 2453	. . . . . 6 |- ( f = ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) -> ( ( f ` 1 ) = y <-> ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) ` 1 ) = y ) )
51	48, 50	anbi12d 710	. . . . 5 |- ( f = ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) -> ( ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) <-> ( ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) ` 0 ) = x /\ ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) ` 1 ) = y ) ) )
52	51	rspcev 3169	. . . 4 |- ( ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) e. ( II Cn { (/) , A } ) /\ ( ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) ` 0 ) = x /\ ( ( z e. ( 0 [,] 1 ) |-> if ( z = 0 , x , y ) ) ` 1 ) = y ) ) -> E. f e. ( II Cn { (/) , A } ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
53	32, 37, 46, 52	syl12anc 1217	. . 3 |- ( ( x e. U. { (/) , A } /\ y e. U. { (/) , A } ) -> E. f e. ( II Cn { (/) , A } ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) )
54	53	rgen2a 2890	. 2 |- A. x e. U. { (/) , A } A. y e. U. { (/) , A } E. f e. ( II Cn { (/) , A } ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y )
55		eqid 2451	. . 3 |- U. { (/) , A } = U. { (/) , A }
56	55	ispcon 27246	. 2 |- ( { (/) , A } e. PCon <-> ( { (/) , A } e. Top /\ A. x e. U. { (/) , A } A. y e. U. { (/) , A } E. f e. ( II Cn { (/) , A } ) ( ( f ` 0 ) = x /\ ( f ` 1 ) = y ) ) )
57	1, 54, 56	mpbir2an 911	1 |- { (/) , A } e. PCon

Syntax hints:   -. wn 3   <-> wb 184   /\ wa 369   = wceq 1370   e. wcel 1758   =/= wne 2644   A.wral 2795   E.wrex 2796   _Vcvv 3068   u. cun 3424   (/)c0 3735   ifcif 3889   {csn 3975   {cpr 3977   U.cuni 4189   |-> cmpt 4448   -->wf 5512   ` cfv 5516  (class class class)co 6190   ^m cmap 7314   0cc0 9383   1c1 9384   [,]cicc 11404   Topctop 18614  TopOnctopon 18615   Cn ccn 18944   IIcii 20567  PConcpcon 27242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-cnex 9439  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459  ax-pre-mulgt0 9460  ax-pre-sup 9461

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-om 6577  df-1st 6677  df-2nd 6678  df-recs 6932  df-rdg 6966  df-er 7201  df-map 7316  df-en 7411  df-dom 7412  df-sdom 7413  df-sup 7792  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-sub 9698  df-neg 9699  df-div 10095  df-nn 10424  df-2 10481  df-3 10482  df-n0 10681  df-z 10748  df-uz 10963  df-q 11055  df-rp 11093  df-xneg 11190  df-xadd 11191  df-xmul 11192  df-icc 11408  df-seq 11908  df-exp 11967  df-cj 12690  df-re 12691  df-im 12692  df-sqr 12826  df-abs 12827  df-topgen 14484  df-psmet 17918  df-xmet 17919  df-met 17920  df-bl 17921  df-mopn 17922  df-top 18619  df-bases 18621  df-topon 18622  df-cn 18947  df-ii 20569  df-pcon 27244

This theorem is referenced by: (None)