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 36765
Description: Lemma for heibor 36775. 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 4007 . . . . . . . . . 10 (𝑒 = 𝐡 β†’ (𝑒 βŠ† βˆͺ 𝑣 ↔ 𝐡 βŠ† βˆͺ 𝑣))
32rexbidv 3178 . . . . . . . . 9 (𝑒 = 𝐡 β†’ (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣))
43notbid 317 . . . . . . . 8 (𝑒 = 𝐡 β†’ (Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣))
5 heibor.3 . . . . . . . 8 𝐾 = {𝑒 ∣ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣}
61, 4, 5elab2 3672 . . . . . . 7 (𝐡 ∈ 𝐾 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣)
76con2bii 357 . . . . . 6 (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 ↔ Β¬ 𝐡 ∈ 𝐾)
87ralbii 3093 . . . . 5 (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 ↔ βˆ€π‘₯ ∈ 𝐴 Β¬ 𝐡 ∈ 𝐾)
9 ralnex 3072 . . . . 5 (βˆ€π‘₯ ∈ 𝐴 Β¬ 𝐡 ∈ 𝐾 ↔ Β¬ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾)
108, 9bitr2i 275 . . . 4 (Β¬ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾 ↔ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣)
11 unieq 4919 . . . . . . . . 9 (𝑣 = (π‘‘β€˜π‘₯) β†’ βˆͺ 𝑣 = βˆͺ (π‘‘β€˜π‘₯))
1211sseq2d 4014 . . . . . . . 8 (𝑣 = (π‘‘β€˜π‘₯) β†’ (𝐡 βŠ† βˆͺ 𝑣 ↔ 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯)))
1312ac6sfi 9289 . . . . . . 7 ((𝐴 ∈ Fin ∧ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣) β†’ βˆƒπ‘‘(𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯)))
1413ex 413 . . . . . 6 (𝐴 ∈ Fin β†’ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 β†’ βˆƒπ‘‘(𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))))
1514adantr 481 . . . . 5 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 β†’ βˆƒπ‘‘(𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))))
16 sseq1 4007 . . . . . . . . . . . 12 (𝑒 = 𝐢 β†’ (𝑒 βŠ† βˆͺ 𝑣 ↔ 𝐢 βŠ† βˆͺ 𝑣))
1716rexbidv 3178 . . . . . . . . . . 11 (𝑒 = 𝐢 β†’ (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣))
1817notbid 317 . . . . . . . . . 10 (𝑒 = 𝐢 β†’ (Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣))
1918, 5elab2g 3670 . . . . . . . . 9 (𝐢 ∈ 𝐾 β†’ (𝐢 ∈ 𝐾 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣))
2019ibi 266 . . . . . . . 8 (𝐢 ∈ 𝐾 β†’ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣)
21 frn 6724 . . . . . . . . . . . . . . 15 (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) β†’ ran 𝑑 βŠ† (𝒫 π‘ˆ ∩ Fin))
2221ad2antrl 726 . . . . . . . . . . . . . 14 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ ran 𝑑 βŠ† (𝒫 π‘ˆ ∩ Fin))
23 inss1 4228 . . . . . . . . . . . . . 14 (𝒫 π‘ˆ ∩ Fin) βŠ† 𝒫 π‘ˆ
2422, 23sstrdi 3994 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ ran 𝑑 βŠ† 𝒫 π‘ˆ)
25 sspwuni 5103 . . . . . . . . . . . . 13 (ran 𝑑 βŠ† 𝒫 π‘ˆ ↔ βˆͺ ran 𝑑 βŠ† π‘ˆ)
2624, 25sylib 217 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 βŠ† π‘ˆ)
27 vex 3478 . . . . . . . . . . . . . . 15 𝑑 ∈ V
2827rnex 7905 . . . . . . . . . . . . . 14 ran 𝑑 ∈ V
2928uniex 7733 . . . . . . . . . . . . 13 βˆͺ ran 𝑑 ∈ V
3029elpw 4606 . . . . . . . . . . . 12 (βˆͺ ran 𝑑 ∈ 𝒫 π‘ˆ ↔ βˆͺ ran 𝑑 βŠ† π‘ˆ)
3126, 30sylibr 233 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 ∈ 𝒫 π‘ˆ)
32 ffn 6717 . . . . . . . . . . . . . . 15 (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) β†’ 𝑑 Fn 𝐴)
3332ad2antrl 726 . . . . . . . . . . . . . 14 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ 𝑑 Fn 𝐴)
34 dffn4 6811 . . . . . . . . . . . . . 14 (𝑑 Fn 𝐴 ↔ 𝑑:𝐴–ontoβ†’ran 𝑑)
3533, 34sylib 217 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ 𝑑:𝐴–ontoβ†’ran 𝑑)
36 fofi 9340 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ 𝑑:𝐴–ontoβ†’ran 𝑑) β†’ ran 𝑑 ∈ Fin)
3735, 36syldan 591 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ ran 𝑑 ∈ Fin)
38 inss2 4229 . . . . . . . . . . . . 13 (𝒫 π‘ˆ ∩ Fin) βŠ† Fin
3922, 38sstrdi 3994 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ ran 𝑑 βŠ† Fin)
40 unifi 9343 . . . . . . . . . . . 12 ((ran 𝑑 ∈ Fin ∧ ran 𝑑 βŠ† Fin) β†’ βˆͺ ran 𝑑 ∈ Fin)
4137, 39, 40syl2anc 584 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 ∈ Fin)
4231, 41elind 4194 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 ∈ (𝒫 π‘ˆ ∩ Fin))
4342adantlr 713 . . . . . . . . 9 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 ∈ (𝒫 π‘ˆ ∩ Fin))
44 simplr 767 . . . . . . . . . 10 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡)
45 fnfvelrn 7082 . . . . . . . . . . . . . . . . . 18 ((𝑑 Fn 𝐴 ∧ π‘₯ ∈ 𝐴) β†’ (π‘‘β€˜π‘₯) ∈ ran 𝑑)
4632, 45sylan 580 . . . . . . . . . . . . . . . . 17 ((𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ π‘₯ ∈ 𝐴) β†’ (π‘‘β€˜π‘₯) ∈ ran 𝑑)
4746adantll 712 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Fin ∧ 𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin)) ∧ π‘₯ ∈ 𝐴) β†’ (π‘‘β€˜π‘₯) ∈ ran 𝑑)
48 elssuni 4941 . . . . . . . . . . . . . . . 16 ((π‘‘β€˜π‘₯) ∈ ran 𝑑 β†’ (π‘‘β€˜π‘₯) βŠ† βˆͺ ran 𝑑)
49 uniss 4916 . . . . . . . . . . . . . . . 16 ((π‘‘β€˜π‘₯) βŠ† βˆͺ ran 𝑑 β†’ βˆͺ (π‘‘β€˜π‘₯) βŠ† βˆͺ βˆͺ ran 𝑑)
5047, 48, 493syl 18 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin)) ∧ π‘₯ ∈ 𝐴) β†’ βˆͺ (π‘‘β€˜π‘₯) βŠ† βˆͺ βˆͺ ran 𝑑)
51 sstr2 3989 . . . . . . . . . . . . . . 15 (𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯) β†’ (βˆͺ (π‘‘β€˜π‘₯) βŠ† βˆͺ βˆͺ ran 𝑑 β†’ 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑))
5250, 51syl5com 31 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin)) ∧ π‘₯ ∈ 𝐴) β†’ (𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯) β†’ 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑))
5352ralimdva 3167 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ 𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin)) β†’ (βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯) β†’ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑))
5453impr 455 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑)
55 iunss 5048 . . . . . . . . . . . 12 (βˆͺ π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑 ↔ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑)
5654, 55sylibr 233 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑)
5756adantlr 713 . . . . . . . . . 10 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑)
5844, 57sstrd 3992 . . . . . . . . 9 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ 𝐢 βŠ† βˆͺ βˆͺ ran 𝑑)
59 unieq 4919 . . . . . . . . . . 11 (𝑣 = βˆͺ ran 𝑑 β†’ βˆͺ 𝑣 = βˆͺ βˆͺ ran 𝑑)
6059sseq2d 4014 . . . . . . . . . 10 (𝑣 = βˆͺ ran 𝑑 β†’ (𝐢 βŠ† βˆͺ 𝑣 ↔ 𝐢 βŠ† βˆͺ βˆͺ ran 𝑑))
6160rspcev 3612 . . . . . . . . 9 ((βˆͺ ran 𝑑 ∈ (𝒫 π‘ˆ ∩ Fin) ∧ 𝐢 βŠ† βˆͺ βˆͺ ran 𝑑) β†’ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣)
6243, 58, 61syl2anc 584 . . . . . . . 8 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣)
6320, 62nsyl3 138 . . . . . . 7 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ Β¬ 𝐢 ∈ 𝐾)
6463ex 413 . . . . . 6 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ ((𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯)) β†’ Β¬ 𝐢 ∈ 𝐾))
6564exlimdv 1936 . . . . 5 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ (βˆƒπ‘‘(𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯)) β†’ Β¬ 𝐢 ∈ 𝐾))
6615, 65syld 47 . . . 4 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 β†’ Β¬ 𝐢 ∈ 𝐾))
6710, 66biimtrid 241 . . 3 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ (Β¬ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾 β†’ Β¬ 𝐢 ∈ 𝐾))
6867con4d 115 . 2 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ (𝐢 ∈ 𝐾 β†’ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾))
69683impia 1117 1 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡 ∧ 𝐢 ∈ 𝐾) β†’ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  {cab 2709  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3474   ∩ cin 3947   βŠ† wss 3948  π’« cpw 4602  βˆͺ cuni 4908  βˆͺ ciun 4997  ran crn 5677   Fn wfn 6538  βŸΆwf 6539  β€“ontoβ†’wfo 6541  β€˜cfv 6543  Fincfn 8941  MetOpencmopn 20940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-om 7858  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-fin 8945
This theorem is referenced by:  heiborlem3  36767  heiborlem10  36774
  Copyright terms: Public domain W3C validator