Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heiborlem1 Structured version   Visualization version   GIF version

Theorem heiborlem1 36983
Description: Lemma for heibor 36993. We work with a fixed open cover π‘ˆ throughout. The set 𝐾 is the set of all subsets of 𝑋 that admit no finite subcover of π‘ˆ. (We wish to prove that 𝐾 is empty.) If a set 𝐢 has no finite subcover, then any finite cover of 𝐢 must contain a set that also has no finite subcover. (Contributed by Jeff Madsen, 23-Jan-2014.)
Hypotheses
Ref Expression
heibor.1 𝐽 = (MetOpenβ€˜π·)
heibor.3 𝐾 = {𝑒 ∣ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣}
heiborlem1.4 𝐡 ∈ V
Assertion
Ref Expression
heiborlem1 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡 ∧ 𝐢 ∈ 𝐾) β†’ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾)
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝑒,𝑣,𝐷   𝑒,𝐡,𝑣   𝑒,𝐽,𝑣,π‘₯   𝑒,π‘ˆ,𝑣,π‘₯   𝑒,𝐢,𝑣   π‘₯,𝐾
Allowed substitution hints:   𝐴(𝑣,𝑒)   𝐡(π‘₯)   𝐢(π‘₯)   𝐾(𝑣,𝑒)

Proof of Theorem heiborlem1
Dummy variable 𝑑 is distinct from all other variables.
StepHypRef Expression
1 heiborlem1.4 . . . . . . . 8 𝐡 ∈ V
2 sseq1 4008 . . . . . . . . . 10 (𝑒 = 𝐡 β†’ (𝑒 βŠ† βˆͺ 𝑣 ↔ 𝐡 βŠ† βˆͺ 𝑣))
32rexbidv 3177 . . . . . . . . 9 (𝑒 = 𝐡 β†’ (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣))
43notbid 317 . . . . . . . 8 (𝑒 = 𝐡 β†’ (Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣))
5 heibor.3 . . . . . . . 8 𝐾 = {𝑒 ∣ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣}
61, 4, 5elab2 3673 . . . . . . 7 (𝐡 ∈ 𝐾 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣)
76con2bii 356 . . . . . 6 (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 ↔ Β¬ 𝐡 ∈ 𝐾)
87ralbii 3092 . . . . 5 (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 ↔ βˆ€π‘₯ ∈ 𝐴 Β¬ 𝐡 ∈ 𝐾)
9 ralnex 3071 . . . . 5 (βˆ€π‘₯ ∈ 𝐴 Β¬ 𝐡 ∈ 𝐾 ↔ Β¬ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾)
108, 9bitr2i 275 . . . 4 (Β¬ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾 ↔ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣)
11 unieq 4920 . . . . . . . . 9 (𝑣 = (π‘‘β€˜π‘₯) β†’ βˆͺ 𝑣 = βˆͺ (π‘‘β€˜π‘₯))
1211sseq2d 4015 . . . . . . . 8 (𝑣 = (π‘‘β€˜π‘₯) β†’ (𝐡 βŠ† βˆͺ 𝑣 ↔ 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯)))
1312ac6sfi 9290 . . . . . . 7 ((𝐴 ∈ Fin ∧ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣) β†’ βˆƒπ‘‘(𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯)))
1413ex 412 . . . . . 6 (𝐴 ∈ Fin β†’ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 β†’ βˆƒπ‘‘(𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))))
1514adantr 480 . . . . 5 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 β†’ βˆƒπ‘‘(𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))))
16 sseq1 4008 . . . . . . . . . . . 12 (𝑒 = 𝐢 β†’ (𝑒 βŠ† βˆͺ 𝑣 ↔ 𝐢 βŠ† βˆͺ 𝑣))
1716rexbidv 3177 . . . . . . . . . . 11 (𝑒 = 𝐢 β†’ (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣))
1817notbid 317 . . . . . . . . . 10 (𝑒 = 𝐢 β†’ (Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣))
1918, 5elab2g 3671 . . . . . . . . 9 (𝐢 ∈ 𝐾 β†’ (𝐢 ∈ 𝐾 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣))
2019ibi 266 . . . . . . . 8 (𝐢 ∈ 𝐾 β†’ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣)
21 frn 6725 . . . . . . . . . . . . . . 15 (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) β†’ ran 𝑑 βŠ† (𝒫 π‘ˆ ∩ Fin))
2221ad2antrl 725 . . . . . . . . . . . . . 14 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ ran 𝑑 βŠ† (𝒫 π‘ˆ ∩ Fin))
23 inss1 4229 . . . . . . . . . . . . . 14 (𝒫 π‘ˆ ∩ Fin) βŠ† 𝒫 π‘ˆ
2422, 23sstrdi 3995 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ ran 𝑑 βŠ† 𝒫 π‘ˆ)
25 sspwuni 5104 . . . . . . . . . . . . 13 (ran 𝑑 βŠ† 𝒫 π‘ˆ ↔ βˆͺ ran 𝑑 βŠ† π‘ˆ)
2624, 25sylib 217 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 βŠ† π‘ˆ)
27 vex 3477 . . . . . . . . . . . . . . 15 𝑑 ∈ V
2827rnex 7906 . . . . . . . . . . . . . 14 ran 𝑑 ∈ V
2928uniex 7734 . . . . . . . . . . . . 13 βˆͺ ran 𝑑 ∈ V
3029elpw 4607 . . . . . . . . . . . 12 (βˆͺ ran 𝑑 ∈ 𝒫 π‘ˆ ↔ βˆͺ ran 𝑑 βŠ† π‘ˆ)
3126, 30sylibr 233 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 ∈ 𝒫 π‘ˆ)
32 ffn 6718 . . . . . . . . . . . . . . 15 (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) β†’ 𝑑 Fn 𝐴)
3332ad2antrl 725 . . . . . . . . . . . . . 14 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ 𝑑 Fn 𝐴)
34 dffn4 6812 . . . . . . . . . . . . . 14 (𝑑 Fn 𝐴 ↔ 𝑑:𝐴–ontoβ†’ran 𝑑)
3533, 34sylib 217 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ 𝑑:𝐴–ontoβ†’ran 𝑑)
36 fofi 9341 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ 𝑑:𝐴–ontoβ†’ran 𝑑) β†’ ran 𝑑 ∈ Fin)
3735, 36syldan 590 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ ran 𝑑 ∈ Fin)
38 inss2 4230 . . . . . . . . . . . . 13 (𝒫 π‘ˆ ∩ Fin) βŠ† Fin
3922, 38sstrdi 3995 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ ran 𝑑 βŠ† Fin)
40 unifi 9344 . . . . . . . . . . . 12 ((ran 𝑑 ∈ Fin ∧ ran 𝑑 βŠ† Fin) β†’ βˆͺ ran 𝑑 ∈ Fin)
4137, 39, 40syl2anc 583 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 ∈ Fin)
4231, 41elind 4195 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 ∈ (𝒫 π‘ˆ ∩ Fin))
4342adantlr 712 . . . . . . . . 9 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 ∈ (𝒫 π‘ˆ ∩ Fin))
44 simplr 766 . . . . . . . . . 10 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡)
45 fnfvelrn 7083 . . . . . . . . . . . . . . . . . 18 ((𝑑 Fn 𝐴 ∧ π‘₯ ∈ 𝐴) β†’ (π‘‘β€˜π‘₯) ∈ ran 𝑑)
4632, 45sylan 579 . . . . . . . . . . . . . . . . 17 ((𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ π‘₯ ∈ 𝐴) β†’ (π‘‘β€˜π‘₯) ∈ ran 𝑑)
4746adantll 711 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Fin ∧ 𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin)) ∧ π‘₯ ∈ 𝐴) β†’ (π‘‘β€˜π‘₯) ∈ ran 𝑑)
48 elssuni 4942 . . . . . . . . . . . . . . . 16 ((π‘‘β€˜π‘₯) ∈ ran 𝑑 β†’ (π‘‘β€˜π‘₯) βŠ† βˆͺ ran 𝑑)
49 uniss 4917 . . . . . . . . . . . . . . . 16 ((π‘‘β€˜π‘₯) βŠ† βˆͺ ran 𝑑 β†’ βˆͺ (π‘‘β€˜π‘₯) βŠ† βˆͺ βˆͺ ran 𝑑)
5047, 48, 493syl 18 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin)) ∧ π‘₯ ∈ 𝐴) β†’ βˆͺ (π‘‘β€˜π‘₯) βŠ† βˆͺ βˆͺ ran 𝑑)
51 sstr2 3990 . . . . . . . . . . . . . . 15 (𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯) β†’ (βˆͺ (π‘‘β€˜π‘₯) βŠ† βˆͺ βˆͺ ran 𝑑 β†’ 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑))
5250, 51syl5com 31 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin)) ∧ π‘₯ ∈ 𝐴) β†’ (𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯) β†’ 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑))
5352ralimdva 3166 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ 𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin)) β†’ (βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯) β†’ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑))
5453impr 454 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑)
55 iunss 5049 . . . . . . . . . . . 12 (βˆͺ π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑 ↔ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑)
5654, 55sylibr 233 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑)
5756adantlr 712 . . . . . . . . . 10 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑)
5844, 57sstrd 3993 . . . . . . . . 9 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ 𝐢 βŠ† βˆͺ βˆͺ ran 𝑑)
59 unieq 4920 . . . . . . . . . . 11 (𝑣 = βˆͺ ran 𝑑 β†’ βˆͺ 𝑣 = βˆͺ βˆͺ ran 𝑑)
6059sseq2d 4015 . . . . . . . . . 10 (𝑣 = βˆͺ ran 𝑑 β†’ (𝐢 βŠ† βˆͺ 𝑣 ↔ 𝐢 βŠ† βˆͺ βˆͺ ran 𝑑))
6160rspcev 3613 . . . . . . . . 9 ((βˆͺ ran 𝑑 ∈ (𝒫 π‘ˆ ∩ Fin) ∧ 𝐢 βŠ† βˆͺ βˆͺ ran 𝑑) β†’ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣)
6243, 58, 61syl2anc 583 . . . . . . . 8 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣)
6320, 62nsyl3 138 . . . . . . 7 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ Β¬ 𝐢 ∈ 𝐾)
6463ex 412 . . . . . 6 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ ((𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯)) β†’ Β¬ 𝐢 ∈ 𝐾))
6564exlimdv 1935 . . . . 5 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ (βˆƒπ‘‘(𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯)) β†’ Β¬ 𝐢 ∈ 𝐾))
6615, 65syld 47 . . . 4 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 β†’ Β¬ 𝐢 ∈ 𝐾))
6710, 66biimtrid 241 . . 3 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ (Β¬ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾 β†’ Β¬ 𝐢 ∈ 𝐾))
6867con4d 115 . 2 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ (𝐢 ∈ 𝐾 β†’ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾))
69683impia 1116 1 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡 ∧ 𝐢 ∈ 𝐾) β†’ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540  βˆƒwex 1780   ∈ wcel 2105  {cab 2708  βˆ€wral 3060  βˆƒwrex 3069  Vcvv 3473   ∩ cin 3948   βŠ† wss 3949  π’« cpw 4603  βˆͺ cuni 4909  βˆͺ ciun 4998  ran crn 5678   Fn wfn 6539  βŸΆwf 6540  β€“ontoβ†’wfo 6542  β€˜cfv 6544  Fincfn 8942  MetOpencmopn 21135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-om 7859  df-1o 8469  df-er 8706  df-en 8943  df-dom 8944  df-fin 8946
This theorem is referenced by:  heiborlem3  36985  heiborlem10  36992
  Copyright terms: Public domain W3C validator