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 36208
Description: Lemma for heibor 36218. 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 3967 . . . . . . . . . 10 (𝑒 = 𝐡 β†’ (𝑒 βŠ† βˆͺ 𝑣 ↔ 𝐡 βŠ† βˆͺ 𝑣))
32rexbidv 3173 . . . . . . . . 9 (𝑒 = 𝐡 β†’ (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣))
43notbid 317 . . . . . . . 8 (𝑒 = 𝐡 β†’ (Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣))
5 heibor.3 . . . . . . . 8 𝐾 = {𝑒 ∣ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣}
61, 4, 5elab2 3632 . . . . . . 7 (𝐡 ∈ 𝐾 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣)
76con2bii 357 . . . . . 6 (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 ↔ Β¬ 𝐡 ∈ 𝐾)
87ralbii 3094 . . . . 5 (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 ↔ βˆ€π‘₯ ∈ 𝐴 Β¬ 𝐡 ∈ 𝐾)
9 ralnex 3073 . . . . 5 (βˆ€π‘₯ ∈ 𝐴 Β¬ 𝐡 ∈ 𝐾 ↔ Β¬ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾)
108, 9bitr2i 275 . . . 4 (Β¬ βˆƒπ‘₯ ∈ 𝐴 𝐡 ∈ 𝐾 ↔ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣)
11 unieq 4874 . . . . . . . . 9 (𝑣 = (π‘‘β€˜π‘₯) β†’ βˆͺ 𝑣 = βˆͺ (π‘‘β€˜π‘₯))
1211sseq2d 3974 . . . . . . . 8 (𝑣 = (π‘‘β€˜π‘₯) β†’ (𝐡 βŠ† βˆͺ 𝑣 ↔ 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯)))
1312ac6sfi 9189 . . . . . . 7 ((𝐴 ∈ Fin ∧ βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣) β†’ βˆƒπ‘‘(𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯)))
1413ex 413 . . . . . 6 (𝐴 ∈ Fin β†’ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 β†’ βˆƒπ‘‘(𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))))
1514adantr 481 . . . . 5 ((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) β†’ (βˆ€π‘₯ ∈ 𝐴 βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐡 βŠ† βˆͺ 𝑣 β†’ βˆƒπ‘‘(𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))))
16 sseq1 3967 . . . . . . . . . . . 12 (𝑒 = 𝐢 β†’ (𝑒 βŠ† βˆͺ 𝑣 ↔ 𝐢 βŠ† βˆͺ 𝑣))
1716rexbidv 3173 . . . . . . . . . . 11 (𝑒 = 𝐢 β†’ (βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣))
1817notbid 317 . . . . . . . . . 10 (𝑒 = 𝐢 β†’ (Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝑒 βŠ† βˆͺ 𝑣 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣))
1918, 5elab2g 3630 . . . . . . . . 9 (𝐢 ∈ 𝐾 β†’ (𝐢 ∈ 𝐾 ↔ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣))
2019ibi 266 . . . . . . . 8 (𝐢 ∈ 𝐾 β†’ Β¬ βˆƒπ‘£ ∈ (𝒫 π‘ˆ ∩ Fin)𝐢 βŠ† βˆͺ 𝑣)
21 frn 6672 . . . . . . . . . . . . . . 15 (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) β†’ ran 𝑑 βŠ† (𝒫 π‘ˆ ∩ Fin))
2221ad2antrl 726 . . . . . . . . . . . . . 14 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ ran 𝑑 βŠ† (𝒫 π‘ˆ ∩ Fin))
23 inss1 4186 . . . . . . . . . . . . . 14 (𝒫 π‘ˆ ∩ Fin) βŠ† 𝒫 π‘ˆ
2422, 23sstrdi 3954 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ ran 𝑑 βŠ† 𝒫 π‘ˆ)
25 sspwuni 5058 . . . . . . . . . . . . 13 (ran 𝑑 βŠ† 𝒫 π‘ˆ ↔ βˆͺ ran 𝑑 βŠ† π‘ˆ)
2624, 25sylib 217 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 βŠ† π‘ˆ)
27 vex 3447 . . . . . . . . . . . . . . 15 𝑑 ∈ V
2827rnex 7841 . . . . . . . . . . . . . 14 ran 𝑑 ∈ V
2928uniex 7670 . . . . . . . . . . . . 13 βˆͺ ran 𝑑 ∈ V
3029elpw 4562 . . . . . . . . . . . 12 (βˆͺ ran 𝑑 ∈ 𝒫 π‘ˆ ↔ βˆͺ ran 𝑑 βŠ† π‘ˆ)
3126, 30sylibr 233 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 ∈ 𝒫 π‘ˆ)
32 ffn 6665 . . . . . . . . . . . . . . 15 (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) β†’ 𝑑 Fn 𝐴)
3332ad2antrl 726 . . . . . . . . . . . . . 14 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ 𝑑 Fn 𝐴)
34 dffn4 6759 . . . . . . . . . . . . . 14 (𝑑 Fn 𝐴 ↔ 𝑑:𝐴–ontoβ†’ran 𝑑)
3533, 34sylib 217 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ 𝑑:𝐴–ontoβ†’ran 𝑑)
36 fofi 9240 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ 𝑑:𝐴–ontoβ†’ran 𝑑) β†’ ran 𝑑 ∈ Fin)
3735, 36syldan 591 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ ran 𝑑 ∈ Fin)
38 inss2 4187 . . . . . . . . . . . . 13 (𝒫 π‘ˆ ∩ Fin) βŠ† Fin
3922, 38sstrdi 3954 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ ran 𝑑 βŠ† Fin)
40 unifi 9243 . . . . . . . . . . . 12 ((ran 𝑑 ∈ Fin ∧ ran 𝑑 βŠ† Fin) β†’ βˆͺ ran 𝑑 ∈ Fin)
4137, 39, 40syl2anc 584 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 ∈ Fin)
4231, 41elind 4152 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 ∈ (𝒫 π‘ˆ ∩ Fin))
4342adantlr 713 . . . . . . . . 9 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ ran 𝑑 ∈ (𝒫 π‘ˆ ∩ Fin))
44 simplr 767 . . . . . . . . . 10 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡)
45 fnfvelrn 7028 . . . . . . . . . . . . . . . . . 18 ((𝑑 Fn 𝐴 ∧ π‘₯ ∈ 𝐴) β†’ (π‘‘β€˜π‘₯) ∈ ran 𝑑)
4632, 45sylan 580 . . . . . . . . . . . . . . . . 17 ((𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ π‘₯ ∈ 𝐴) β†’ (π‘‘β€˜π‘₯) ∈ ran 𝑑)
4746adantll 712 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ Fin ∧ 𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin)) ∧ π‘₯ ∈ 𝐴) β†’ (π‘‘β€˜π‘₯) ∈ ran 𝑑)
48 elssuni 4896 . . . . . . . . . . . . . . . 16 ((π‘‘β€˜π‘₯) ∈ ran 𝑑 β†’ (π‘‘β€˜π‘₯) βŠ† βˆͺ ran 𝑑)
49 uniss 4871 . . . . . . . . . . . . . . . 16 ((π‘‘β€˜π‘₯) βŠ† βˆͺ ran 𝑑 β†’ βˆͺ (π‘‘β€˜π‘₯) βŠ† βˆͺ βˆͺ ran 𝑑)
5047, 48, 493syl 18 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Fin ∧ 𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin)) ∧ π‘₯ ∈ 𝐴) β†’ βˆͺ (π‘‘β€˜π‘₯) βŠ† βˆͺ βˆͺ ran 𝑑)
51 sstr2 3949 . . . . . . . . . . . . . . 15 (𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯) β†’ (βˆͺ (π‘‘β€˜π‘₯) βŠ† βˆͺ βˆͺ ran 𝑑 β†’ 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑))
5250, 51syl5com 31 . . . . . . . . . . . . . 14 (((𝐴 ∈ Fin ∧ 𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin)) ∧ π‘₯ ∈ 𝐴) β†’ (𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯) β†’ 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑))
5352ralimdva 3162 . . . . . . . . . . . . 13 ((𝐴 ∈ Fin ∧ 𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin)) β†’ (βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯) β†’ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑))
5453impr 455 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑)
55 iunss 5003 . . . . . . . . . . . 12 (βˆͺ π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑 ↔ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑)
5654, 55sylibr 233 . . . . . . . . . . 11 ((𝐴 ∈ Fin ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑)
5756adantlr 713 . . . . . . . . . 10 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ βˆͺ π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ βˆͺ ran 𝑑)
5844, 57sstrd 3952 . . . . . . . . 9 (((𝐴 ∈ Fin ∧ 𝐢 βŠ† βˆͺ π‘₯ ∈ 𝐴 𝐡) ∧ (𝑑:𝐴⟢(𝒫 π‘ˆ ∩ Fin) ∧ βˆ€π‘₯ ∈ 𝐴 𝐡 βŠ† βˆͺ (π‘‘β€˜π‘₯))) β†’ 𝐢 βŠ† βˆͺ βˆͺ ran 𝑑)
59 unieq 4874 . . . . . . . . . . 11 (𝑣 = βˆͺ ran 𝑑 β†’ βˆͺ 𝑣 = βˆͺ βˆͺ ran 𝑑)
6059sseq2d 3974 . . . . . . . . . 10 (𝑣 = βˆͺ ran 𝑑 β†’ (𝐢 βŠ† βˆͺ 𝑣 ↔ 𝐢 βŠ† βˆͺ βˆͺ ran 𝑑))
6160rspcev 3579 . . . . . . . . 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 2714  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3443   ∩ cin 3907   βŠ† wss 3908  π’« cpw 4558  βˆͺ cuni 4863  βˆͺ ciun 4952  ran crn 5632   Fn wfn 6488  βŸΆwf 6489  β€“ontoβ†’wfo 6491  β€˜cfv 6493  Fincfn 8841  MetOpencmopn 20739
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 2708  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7664
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-iun 4954  df-br 5104  df-opab 5166  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-om 7795  df-1o 8404  df-er 8606  df-en 8842  df-dom 8843  df-fin 8845
This theorem is referenced by:  heiborlem3  36210  heiborlem10  36217
  Copyright terms: Public domain W3C validator