Metamath Proof Explorer

Theorem mreexexd

Description: Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if F and G are disjoint from H , ( F u. H ) is independent, F is contained in the closure of ( G u. H ) , and either F or G is finite, then there is a subset q of G equinumerous to F such that ( q u. H ) is independent. This implies the case of Proposition 4.2.1 in FaureFrolicher p. 86 where either ( A \ B ) or ( B \ A ) is finite. The theorem is proven by induction using mreexexlem3d for the base case and mreexexlem4d for the induction step. (Contributed by David Moews, 1-May-2017) Remove dependencies on ax-rep and ax-ac2 . (Revised by Brendan Leahy, 2-Jun-2021)

Ref Expression
Hypotheses mreexexlem2d.1 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
mreexexlem2d.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
mreexexlem2d.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
mreexexlem2d.4 ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
mreexexlem2d.5 ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑋 ∖ 𝐻 ) )
mreexexlem2d.6 ⊢ ( 𝜑 → 𝐺 ⊆ ( 𝑋 ∖ 𝐻 ) )
mreexexlem2d.7 ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
mreexexlem2d.8 ⊢ ( 𝜑 → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
mreexexd.9 ⊢ ( 𝜑 → ( 𝐹 ∈ Fin ∨ 𝐺 ∈ Fin ) )
Assertion mreexexd ( 𝜑 → ∃ 𝑞 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑞 ∧ ( 𝑞 ∪ 𝐻 ) ∈ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 mreexexlem2d.1 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
2 mreexexlem2d.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3 mreexexlem2d.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4 mreexexlem2d.4 ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
5 mreexexlem2d.5 ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑋 ∖ 𝐻 ) )
6 mreexexlem2d.6 ⊢ ( 𝜑 → 𝐺 ⊆ ( 𝑋 ∖ 𝐻 ) )
7 mreexexlem2d.7 ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
8 mreexexlem2d.8 ⊢ ( 𝜑 → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
9 mreexexd.9 ⊢ ( 𝜑 → ( 𝐹 ∈ Fin ∨ 𝐺 ∈ Fin ) )
10 1 elfvexd ⊢ ( 𝜑 → 𝑋 ∈ V )
11 exmid ⊢ ( 𝐹 ∈ Fin ∨ ¬ 𝐹 ∈ Fin )
12 ficardid ⊢ ( 𝐹 ∈ Fin → ( card ‘ 𝐹 ) ≈ 𝐹 )
13 12 ensymd ⊢ ( 𝐹 ∈ Fin → 𝐹 ≈ ( card ‘ 𝐹 ) )
14 iftrue ⊢ ( 𝐹 ∈ Fin → if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) = ( card ‘ 𝐹 ) )
15 13 14 breqtrrd ⊢ ( 𝐹 ∈ Fin → 𝐹 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) )
16 15 a1i ⊢ ( 𝜑 → ( 𝐹 ∈ Fin → 𝐹 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) )
17 9 orcanai ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ Fin ) → 𝐺 ∈ Fin )
18 ficardid ⊢ ( 𝐺 ∈ Fin → ( card ‘ 𝐺 ) ≈ 𝐺 )
19 18 ensymd ⊢ ( 𝐺 ∈ Fin → 𝐺 ≈ ( card ‘ 𝐺 ) )
20 17 19 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ Fin ) → 𝐺 ≈ ( card ‘ 𝐺 ) )
21 iffalse ⊢ ( ¬ 𝐹 ∈ Fin → if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) = ( card ‘ 𝐺 ) )
22 21 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ Fin ) → if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) = ( card ‘ 𝐺 ) )
23 20 22 breqtrrd ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ Fin ) → 𝐺 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) )
24 23 ex ⊢ ( 𝜑 → ( ¬ 𝐹 ∈ Fin → 𝐺 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) )
25 16 24 orim12d ⊢ ( 𝜑 → ( ( 𝐹 ∈ Fin ∨ ¬ 𝐹 ∈ Fin ) → ( 𝐹 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ∨ 𝐺 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) ) )
26 11 25 mpi ⊢ ( 𝜑 → ( 𝐹 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ∨ 𝐺 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) )
27 ficardom ⊢ ( 𝐹 ∈ Fin → ( card ‘ 𝐹 ) ∈ ω )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ Fin ) → ( card ‘ 𝐹 ) ∈ ω )
29 ficardom ⊢ ( 𝐺 ∈ Fin → ( card ‘ 𝐺 ) ∈ ω )
30 17 29 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ Fin ) → ( card ‘ 𝐺 ) ∈ ω )
31 28 30 ifclda ⊢ ( 𝜑 → if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ∈ ω )
32 breq2 ⊢ ( 𝑙 = ∅ → ( 𝑓 ≈ 𝑙 ↔ 𝑓 ≈ ∅ ) )
33 breq2 ⊢ ( 𝑙 = ∅ → ( 𝑔 ≈ 𝑙 ↔ 𝑔 ≈ ∅ ) )
34 32 33 orbi12d ⊢ ( 𝑙 = ∅ → ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ↔ ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ) )
35 34 3anbi1d ⊢ ( 𝑙 = ∅ → ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ↔ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) )
36 35 imbi1d ⊢ ( 𝑙 = ∅ → ( ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ( ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
37 36 2ralbidv ⊢ ( 𝑙 = ∅ → ( ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
38 37 albidv ⊢ ( 𝑙 = ∅ → ( ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
39 38 imbi2d ⊢ ( 𝑙 = ∅ → ( ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ↔ ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ) )
40 breq2 ⊢ ( 𝑙 = 𝑘 → ( 𝑓 ≈ 𝑙 ↔ 𝑓 ≈ 𝑘 ) )
41 breq2 ⊢ ( 𝑙 = 𝑘 → ( 𝑔 ≈ 𝑙 ↔ 𝑔 ≈ 𝑘 ) )
42 40 41 orbi12d ⊢ ( 𝑙 = 𝑘 → ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ↔ ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ) )
43 42 3anbi1d ⊢ ( 𝑙 = 𝑘 → ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ↔ ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) )
44 43 imbi1d ⊢ ( 𝑙 = 𝑘 → ( ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
45 44 2ralbidv ⊢ ( 𝑙 = 𝑘 → ( ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
46 45 albidv ⊢ ( 𝑙 = 𝑘 → ( ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
47 46 imbi2d ⊢ ( 𝑙 = 𝑘 → ( ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ↔ ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ) )
48 breq2 ⊢ ( 𝑙 = suc 𝑘 → ( 𝑓 ≈ 𝑙 ↔ 𝑓 ≈ suc 𝑘 ) )
49 breq2 ⊢ ( 𝑙 = suc 𝑘 → ( 𝑔 ≈ 𝑙 ↔ 𝑔 ≈ suc 𝑘 ) )
50 48 49 orbi12d ⊢ ( 𝑙 = suc 𝑘 → ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ↔ ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ) )
51 50 3anbi1d ⊢ ( 𝑙 = suc 𝑘 → ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ↔ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) )
52 51 imbi1d ⊢ ( 𝑙 = suc 𝑘 → ( ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
53 52 2ralbidv ⊢ ( 𝑙 = suc 𝑘 → ( ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
54 53 albidv ⊢ ( 𝑙 = suc 𝑘 → ( ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
55 54 imbi2d ⊢ ( 𝑙 = suc 𝑘 → ( ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ↔ ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ) )
56 breq2 ⊢ ( 𝑙 = if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) → ( 𝑓 ≈ 𝑙 ↔ 𝑓 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) )
57 breq2 ⊢ ( 𝑙 = if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) → ( 𝑔 ≈ 𝑙 ↔ 𝑔 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) )
58 56 57 orbi12d ⊢ ( 𝑙 = if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) → ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ↔ ( 𝑓 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ∨ 𝑔 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) ) )
59 58 3anbi1d ⊢ ( 𝑙 = if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) → ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ↔ ( ( 𝑓 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ∨ 𝑔 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) )
60 59 imbi1d ⊢ ( 𝑙 = if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) → ( ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ( ( ( 𝑓 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ∨ 𝑔 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
61 60 2ralbidv ⊢ ( 𝑙 = if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) → ( ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ∨ 𝑔 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
62 61 albidv ⊢ ( 𝑙 = if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) → ( ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ∨ 𝑔 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
63 62 imbi2d ⊢ ( 𝑙 = if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) → ( ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑙 ∨ 𝑔 ≈ 𝑙 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ↔ ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ∨ 𝑔 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ) )
64 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
65 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
66 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) )
67 66 elpwid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝑓 ⊆ ( 𝑋 ∖ ℎ ) )
68 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) )
69 68 elpwid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝑔 ⊆ ( 𝑋 ∖ ℎ ) )
70 simpr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) )
71 simpr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → ( 𝑓 ∪ ℎ ) ∈ 𝐼 )
72 simpr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) )
73 en0 ⊢ ( 𝑓 ≈ ∅ ↔ 𝑓 = ∅ )
74 en0 ⊢ ( 𝑔 ≈ ∅ ↔ 𝑔 = ∅ )
75 73 74 orbi12i ⊢ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ↔ ( 𝑓 = ∅ ∨ 𝑔 = ∅ ) )
76 72 75 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → ( 𝑓 = ∅ ∨ 𝑔 = ∅ ) )
77 64 2 3 65 67 69 70 71 76 mreexexlem3d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) )
78 77 ex ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) → ( ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) )
79 78 ralrimivva ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) )
80 79 alrimiv ⊢ ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ ∅ ∨ 𝑔 ≈ ∅ ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) )
81 nfv ⊢ Ⅎ ℎ 𝜑
82 nfv ⊢ Ⅎ ℎ 𝑘 ∈ ω
83 nfa1 ⊢ Ⅎ ℎ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) )
84 81 82 83 nf3an ⊢ Ⅎ ℎ ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) )
85 nfv ⊢ Ⅎ 𝑓 𝜑
86 nfv ⊢ Ⅎ 𝑓 𝑘 ∈ ω
87 nfra1 ⊢ Ⅎ 𝑓 ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) )
88 87 nfal ⊢ Ⅎ 𝑓 ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) )
89 85 86 88 nf3an ⊢ Ⅎ 𝑓 ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) )
90 nfv ⊢ Ⅎ 𝑔 𝜑
91 nfv ⊢ Ⅎ 𝑔 𝑘 ∈ ω
92 nfra2w ⊢ Ⅎ 𝑔 ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) )
93 92 nfal ⊢ Ⅎ 𝑔 ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) )
94 90 91 93 nf3an ⊢ Ⅎ 𝑔 ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) )
95 nfv ⊢ Ⅎ 𝑔 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ )
96 94 95 nfan ⊢ Ⅎ 𝑔 ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) )
97 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
98 97 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
99 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
100 99 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
101 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) )
102 101 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝑓 ⊆ ( 𝑋 ∖ ℎ ) )
103 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) )
104 103 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝑔 ⊆ ( 𝑋 ∖ ℎ ) )
105 simpr2 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) )
106 simpr3 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → ( 𝑓 ∪ ℎ ) ∈ 𝐼 )
107 simpll2 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → 𝑘 ∈ ω )
108 simpll3 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) )
109 simpr1 ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) )
110 98 2 3 100 102 104 105 106 107 108 109 mreexexlem4d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) ∧ ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) )
111 110 ex ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∧ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) ) → ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) )
112 111 expr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) → ( 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) → ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
113 96 112 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ∧ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ) → ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) )
114 113 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) → ( 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) → ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
115 89 114 ralrimi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) → ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) )
116 84 115 alrimi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ω ∧ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) )
117 116 3exp ⊢ ( 𝜑 → ( 𝑘 ∈ ω → ( ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ) )
118 117 com12 ⊢ ( 𝑘 ∈ ω → ( 𝜑 → ( ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ) )
119 118 a2d ⊢ ( 𝑘 ∈ ω → ( ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝑘 ∨ 𝑔 ≈ 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) → ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ suc 𝑘 ∨ 𝑔 ≈ suc 𝑘 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) ) )
120 39 47 55 63 80 119 finds ⊢ ( if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ∈ ω → ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ∨ 𝑔 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) ) )
121 31 120 mpcom ⊢ ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ∨ 𝑔 ≈ if ( 𝐹 ∈ Fin , ( card ‘ 𝐹 ) , ( card ‘ 𝐺 ) ) ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑖 ∧ ( 𝑖 ∪ ℎ ) ∈ 𝐼 ) ) )
122 10 5 6 7 8 26 121 mreexexlemd ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑞 ∧ ( 𝑞 ∪ 𝐻 ) ∈ 𝐼 ) )