Theorem hmph 11030

Description: Express the predicate J is homeomorph to K.

Assertion

Ref	Expression
hmph	⊢ ((J ∈ Top ⋀ K ∈ Top) → (J ~= K ↔ ∃f f ∈ (J Homeo K)))

Distinct variable groups:   f,J   f,K

Proof of Theorem hmph

Step	Hyp	Ref	Expression
1		eleq1 1577	. . . 4 ⊢ (j = J → (j ∈ Top ↔ J ∈ Top))
2		opreq1 4026	. . . . . 6 ⊢ (j = J → (j Homeo k) = (J Homeo k))
3	2	eleq2d 1584	. . . . 5 ⊢ (j = J → (f ∈ (j Homeo k) ↔ f ∈ (J Homeo k)))
4	3	exbidv 1317	. . . 4 ⊢ (j = J → (∃f f ∈ (j Homeo k) ↔ ∃f f ∈ (J Homeo k)))
5	1, 4	3anbi13d 901	. . 3 ⊢ (j = J → ((j ∈ Top ⋀ k ∈ Top ⋀ ∃f f ∈ (j Homeo k)) ↔ (J ∈ Top ⋀ k ∈ Top ⋀ ∃f f ∈ (J Homeo k))))
6		eleq1 1577	. . . . . 6 ⊢ (k = K → (k ∈ Top ↔ K ∈ Top))
7	6	bicomd 524	. . . . 5 ⊢ (k = K → (K ∈ Top ↔ k ∈ Top))
8		opreq2 4027	. . . . . . . 8 ⊢ (K = k → (J Homeo K) = (J Homeo k))
9	8	eqcoms 1521	. . . . . . 7 ⊢ (k = K → (J Homeo K) = (J Homeo k))
10	9	eleq2d 1584	. . . . . 6 ⊢ (k = K → (f ∈ (J Homeo K) ↔ f ∈ (J Homeo k)))
11	10	exbidv 1317	. . . . 5 ⊢ (k = K → (∃f f ∈ (J Homeo K) ↔ ∃f f ∈ (J Homeo k)))
12	7, 11	3anbi23d 902	. . . 4 ⊢ (k = K → ((J ∈ Top ⋀ K ∈ Top ⋀ ∃f f ∈ (J Homeo K)) ↔ (J ∈ Top ⋀ k ∈ Top ⋀ ∃f f ∈ (J Homeo k))))
13		df-3an 783	. . . 4 ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ ∃f f ∈ (J Homeo K)) ↔ ((J ∈ Top ⋀ K ∈ Top) ⋀ ∃f f ∈ (J Homeo K)))
14	12, 13	syl5rbbr 538	. . 3 ⊢ (k = K → ((J ∈ Top ⋀ k ∈ Top ⋀ ∃f f ∈ (J Homeo k)) ↔ ((J ∈ Top ⋀ K ∈ Top) ⋀ ∃f f ∈ (J Homeo K))))
15		df-hmph 11029	. . 3 ⊢ ~= = {<.j, k>.∣(j ∈ Top ⋀ k ∈ Top ⋀ ∃f f ∈ (j Homeo k))}
16	5, 14, 15	brabg 2895	. 2 ⊢ ((J ∈ Top ⋀ K ∈ Top) → (J ~= K ↔ ((J ∈ Top ⋀ K ∈ Top) ⋀ ∃f f ∈ (J Homeo K))))
17	16	bianabs 656	1 ⊢ ((J ∈ Top ⋀ K ∈ Top) → (J ~= K ↔ ∃f f ∈ (J Homeo K)))

Syntax hints:   → wi 3   ↔ wb 144   ⋀ wa 221   ⋀ w3a 781   = wceq 992   ∈ wcel 994  ∃wex 1016   class class class wbr 2692  (class class class)co 4021  Topctop 7800   Homeo chomeosm 11019   ~= chomeo 11020

This theorem is referenced by:  hmphsyma 11034  hmphre 11036  hmphtr 11037  homcard 11045  homcardus 11046  eqindhome 11047  comptoppr 11495  conntoppr 11504  reheibor 12081

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-xp 3265  df-cnv 3267  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fv 3279  df-opr 4023  df-hmph 11029

Copyright terms: Public domain