Metamath Proof Explorer

Theorem mreexexlem4d

Description: Induction step of the induction in mreexexd . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mreexexlem2d.1 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
mreexexlem2d.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
mreexexlem2d.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
mreexexlem2d.4 ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
mreexexlem2d.5 ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑋 ∖ 𝐻 ) )
mreexexlem2d.6 ⊢ ( 𝜑 → 𝐺 ⊆ ( 𝑋 ∖ 𝐻 ) )
mreexexlem2d.7 ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
mreexexlem2d.8 ⊢ ( 𝜑 → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
mreexexlem4d.9 ⊢ ( 𝜑 → 𝐿 ∈ ω )
mreexexlem4d.A ⊢ ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐿 ∨ 𝑔 ≈ 𝐿 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) )
mreexexlem4d.B ⊢ ( 𝜑 → ( 𝐹 ≈ suc 𝐿 ∨ 𝐺 ≈ suc 𝐿 ) )
Assertion mreexexlem4d ( 𝜑 → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )

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 mreexexlem4d.9 ⊢ ( 𝜑 → 𝐿 ∈ ω )
10 mreexexlem4d.A ⊢ ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐿 ∨ 𝑔 ≈ 𝐿 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) )
11 mreexexlem4d.B ⊢ ( 𝜑 → ( 𝐹 ≈ suc 𝐿 ∨ 𝐺 ≈ suc 𝐿 ) )
12 1 adantr ⊢ ( ( 𝜑 ∧ 𝐹 = ∅ ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
13 4 adantr ⊢ ( ( 𝜑 ∧ 𝐹 = ∅ ) → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
14 5 adantr ⊢ ( ( 𝜑 ∧ 𝐹 = ∅ ) → 𝐹 ⊆ ( 𝑋 ∖ 𝐻 ) )
15 6 adantr ⊢ ( ( 𝜑 ∧ 𝐹 = ∅ ) → 𝐺 ⊆ ( 𝑋 ∖ 𝐻 ) )
16 7 adantr ⊢ ( ( 𝜑 ∧ 𝐹 = ∅ ) → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
17 8 adantr ⊢ ( ( 𝜑 ∧ 𝐹 = ∅ ) → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
18 animorrl ⊢ ( ( 𝜑 ∧ 𝐹 = ∅ ) → ( 𝐹 = ∅ ∨ 𝐺 = ∅ ) )
19 12 2 3 13 14 15 16 17 18 mreexexlem3d ⊢ ( ( 𝜑 ∧ 𝐹 = ∅ ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )
20 n0 ⊢ ( 𝐹 ≠ ∅ ↔ ∃ 𝑟 𝑟 ∈ 𝐹 )
21 20 bilani ⊢ ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) → ∃ 𝑟 𝑟 ∈ 𝐹 )
22 1 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
23 4 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
24 5 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) → 𝐹 ⊆ ( 𝑋 ∖ 𝐻 ) )
25 6 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) → 𝐺 ⊆ ( 𝑋 ∖ 𝐻 ) )
26 7 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
27 8 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
28 simpr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) → 𝑟 ∈ 𝐹 )
29 22 2 3 23 24 25 26 27 28 mreexexlem2d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) → ∃ 𝑞 ∈ 𝐺 ( ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) )
30 3anass ⊢ ( ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ↔ ( 𝑞 ∈ 𝐺 ∧ ( ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) )
31 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
32 31 elfvexd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → 𝑋 ∈ V )
33 simpr2 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) )
34 difsnb ⊢ ( ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ↔ ( ( 𝐹 ∖ { 𝑟 } ) ∖ { 𝑞 } ) = ( 𝐹 ∖ { 𝑟 } ) )
35 33 34 sylib ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( ( 𝐹 ∖ { 𝑟 } ) ∖ { 𝑞 } ) = ( 𝐹 ∖ { 𝑟 } ) )
36 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → 𝐹 ⊆ ( 𝑋 ∖ 𝐻 ) )
37 36 ssdifssd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( 𝐹 ∖ { 𝑟 } ) ⊆ ( 𝑋 ∖ 𝐻 ) )
38 37 ssdifd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( ( 𝐹 ∖ { 𝑟 } ) ∖ { 𝑞 } ) ⊆ ( ( 𝑋 ∖ 𝐻 ) ∖ { 𝑞 } ) )
39 35 38 eqsstrrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( 𝐹 ∖ { 𝑟 } ) ⊆ ( ( 𝑋 ∖ 𝐻 ) ∖ { 𝑞 } ) )
40 difun1 ⊢ ( 𝑋 ∖ ( 𝐻 ∪ { 𝑞 } ) ) = ( ( 𝑋 ∖ 𝐻 ) ∖ { 𝑞 } )
41 39 40 sseqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( 𝐹 ∖ { 𝑟 } ) ⊆ ( 𝑋 ∖ ( 𝐻 ∪ { 𝑞 } ) ) )
42 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → 𝐺 ⊆ ( 𝑋 ∖ 𝐻 ) )
43 42 ssdifd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( 𝐺 ∖ { 𝑞 } ) ⊆ ( ( 𝑋 ∖ 𝐻 ) ∖ { 𝑞 } ) )
44 43 40 sseqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( 𝐺 ∖ { 𝑞 } ) ⊆ ( 𝑋 ∖ ( 𝐻 ∪ { 𝑞 } ) ) )
45 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
46 simpr1 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → 𝑞 ∈ 𝐺 )
47 uncom ⊢ ( 𝐻 ∪ { 𝑞 } ) = ( { 𝑞 } ∪ 𝐻 )
48 47 uneq2i ⊢ ( ( 𝐺 ∖ { 𝑞 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) = ( ( 𝐺 ∖ { 𝑞 } ) ∪ ( { 𝑞 } ∪ 𝐻 ) )
49 unass ⊢ ( ( ( 𝐺 ∖ { 𝑞 } ) ∪ { 𝑞 } ) ∪ 𝐻 ) = ( ( 𝐺 ∖ { 𝑞 } ) ∪ ( { 𝑞 } ∪ 𝐻 ) )
50 difsnid ⊢ ( 𝑞 ∈ 𝐺 → ( ( 𝐺 ∖ { 𝑞 } ) ∪ { 𝑞 } ) = 𝐺 )
51 50 uneq1d ⊢ ( 𝑞 ∈ 𝐺 → ( ( ( 𝐺 ∖ { 𝑞 } ) ∪ { 𝑞 } ) ∪ 𝐻 ) = ( 𝐺 ∪ 𝐻 ) )
52 49 51 eqtr3id ⊢ ( 𝑞 ∈ 𝐺 → ( ( 𝐺 ∖ { 𝑞 } ) ∪ ( { 𝑞 } ∪ 𝐻 ) ) = ( 𝐺 ∪ 𝐻 ) )
53 48 52 eqtrid ⊢ ( 𝑞 ∈ 𝐺 → ( ( 𝐺 ∖ { 𝑞 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) = ( 𝐺 ∪ 𝐻 ) )
54 46 53 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( ( 𝐺 ∖ { 𝑞 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) = ( 𝐺 ∪ 𝐻 ) )
55 54 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( 𝑁 ‘ ( ( 𝐺 ∖ { 𝑞 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ) = ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
56 45 55 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → 𝐹 ⊆ ( 𝑁 ‘ ( ( 𝐺 ∖ { 𝑞 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ) )
57 56 ssdifssd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( 𝐹 ∖ { 𝑟 } ) ⊆ ( 𝑁 ‘ ( ( 𝐺 ∖ { 𝑞 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ) )
58 simpr3 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 )
59 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( 𝐹 ≈ suc 𝐿 ∨ 𝐺 ≈ suc 𝐿 ) )
60 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → 𝐿 ∈ ω )
61 simplr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → 𝑟 ∈ 𝐹 )
62 3anan12 ⊢ ( ( 𝐿 ∈ ω ∧ 𝐹 ≈ suc 𝐿 ∧ 𝑟 ∈ 𝐹 ) ↔ ( 𝐹 ≈ suc 𝐿 ∧ ( 𝐿 ∈ ω ∧ 𝑟 ∈ 𝐹 ) ) )
63 dif1ennn ⊢ ( ( 𝐿 ∈ ω ∧ 𝐹 ≈ suc 𝐿 ∧ 𝑟 ∈ 𝐹 ) → ( 𝐹 ∖ { 𝑟 } ) ≈ 𝐿 )
64 62 63 sylbir ⊢ ( ( 𝐹 ≈ suc 𝐿 ∧ ( 𝐿 ∈ ω ∧ 𝑟 ∈ 𝐹 ) ) → ( 𝐹 ∖ { 𝑟 } ) ≈ 𝐿 )
65 64 expcom ⊢ ( ( 𝐿 ∈ ω ∧ 𝑟 ∈ 𝐹 ) → ( 𝐹 ≈ suc 𝐿 → ( 𝐹 ∖ { 𝑟 } ) ≈ 𝐿 ) )
66 60 61 65 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( 𝐹 ≈ suc 𝐿 → ( 𝐹 ∖ { 𝑟 } ) ≈ 𝐿 ) )
67 3anan12 ⊢ ( ( 𝐿 ∈ ω ∧ 𝐺 ≈ suc 𝐿 ∧ 𝑞 ∈ 𝐺 ) ↔ ( 𝐺 ≈ suc 𝐿 ∧ ( 𝐿 ∈ ω ∧ 𝑞 ∈ 𝐺 ) ) )
68 dif1ennn ⊢ ( ( 𝐿 ∈ ω ∧ 𝐺 ≈ suc 𝐿 ∧ 𝑞 ∈ 𝐺 ) → ( 𝐺 ∖ { 𝑞 } ) ≈ 𝐿 )
69 67 68 sylbir ⊢ ( ( 𝐺 ≈ suc 𝐿 ∧ ( 𝐿 ∈ ω ∧ 𝑞 ∈ 𝐺 ) ) → ( 𝐺 ∖ { 𝑞 } ) ≈ 𝐿 )
70 69 expcom ⊢ ( ( 𝐿 ∈ ω ∧ 𝑞 ∈ 𝐺 ) → ( 𝐺 ≈ suc 𝐿 → ( 𝐺 ∖ { 𝑞 } ) ≈ 𝐿 ) )
71 60 46 70 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( 𝐺 ≈ suc 𝐿 → ( 𝐺 ∖ { 𝑞 } ) ≈ 𝐿 ) )
72 66 71 orim12d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( ( 𝐹 ≈ suc 𝐿 ∨ 𝐺 ≈ suc 𝐿 ) → ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝐿 ∨ ( 𝐺 ∖ { 𝑞 } ) ≈ 𝐿 ) ) )
73 59 72 mpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝐿 ∨ ( 𝐺 ∖ { 𝑞 } ) ≈ 𝐿 ) )
74 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐿 ∨ 𝑔 ≈ 𝐿 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) )
75 32 41 44 57 58 73 74 mreexexlemd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ∃ 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) )
76 32 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → 𝑋 ∈ V )
77 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → 𝐺 ⊆ ( 𝑋 ∖ 𝐻 ) )
78 77 difss2d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → 𝐺 ⊆ 𝑋 )
79 76 78 ssexd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → 𝐺 ∈ V )
80 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) )
81 80 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → 𝑖 ⊆ ( 𝐺 ∖ { 𝑞 } ) )
82 81 difss2d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → 𝑖 ⊆ 𝐺 )
83 simplr1 ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → 𝑞 ∈ 𝐺 )
84 83 snssd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → { 𝑞 } ⊆ 𝐺 )
85 82 84 unssd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → ( 𝑖 ∪ { 𝑞 } ) ⊆ 𝐺 )
86 79 85 sselpwd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → ( 𝑖 ∪ { 𝑞 } ) ∈ 𝒫 𝐺 )
87 difsnid ⊢ ( 𝑟 ∈ 𝐹 → ( ( 𝐹 ∖ { 𝑟 } ) ∪ { 𝑟 } ) = 𝐹 )
88 87 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → ( ( 𝐹 ∖ { 𝑟 } ) ∪ { 𝑟 } ) = 𝐹 )
89 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 )
90 en2sn ⊢ ( ( 𝑟 ∈ V ∧ 𝑞 ∈ V ) → { 𝑟 } ≈ { 𝑞 } )
91 90 el2v ⊢ { 𝑟 } ≈ { 𝑞 }
92 91 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → { 𝑟 } ≈ { 𝑞 } )
93 disjdifr ⊢ ( ( 𝐹 ∖ { 𝑟 } ) ∩ { 𝑟 } ) = ∅
94 93 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → ( ( 𝐹 ∖ { 𝑟 } ) ∩ { 𝑟 } ) = ∅ )
95 ssdifin0 ⊢ ( 𝑖 ⊆ ( 𝐺 ∖ { 𝑞 } ) → ( 𝑖 ∩ { 𝑞 } ) = ∅ )
96 81 95 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → ( 𝑖 ∩ { 𝑞 } ) = ∅ )
97 unen ⊢ ( ( ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ { 𝑟 } ≈ { 𝑞 } ) ∧ ( ( ( 𝐹 ∖ { 𝑟 } ) ∩ { 𝑟 } ) = ∅ ∧ ( 𝑖 ∩ { 𝑞 } ) = ∅ ) ) → ( ( 𝐹 ∖ { 𝑟 } ) ∪ { 𝑟 } ) ≈ ( 𝑖 ∪ { 𝑞 } ) )
98 89 92 94 96 97 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → ( ( 𝐹 ∖ { 𝑟 } ) ∪ { 𝑟 } ) ≈ ( 𝑖 ∪ { 𝑞 } ) )
99 88 98 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → 𝐹 ≈ ( 𝑖 ∪ { 𝑞 } ) )
100 unass ⊢ ( ( 𝑖 ∪ { 𝑞 } ) ∪ 𝐻 ) = ( 𝑖 ∪ ( { 𝑞 } ∪ 𝐻 ) )
101 uncom ⊢ ( { 𝑞 } ∪ 𝐻 ) = ( 𝐻 ∪ { 𝑞 } )
102 101 uneq2i ⊢ ( 𝑖 ∪ ( { 𝑞 } ∪ 𝐻 ) ) = ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) )
103 100 102 eqtr2i ⊢ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) = ( ( 𝑖 ∪ { 𝑞 } ) ∪ 𝐻 )
104 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 )
105 103 104 eqeltrrid ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → ( ( 𝑖 ∪ { 𝑞 } ) ∪ 𝐻 ) ∈ 𝐼 )
106 breq2 ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑞 } ) → ( 𝐹 ≈ 𝑗 ↔ 𝐹 ≈ ( 𝑖 ∪ { 𝑞 } ) ) )
107 uneq1 ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑞 } ) → ( 𝑗 ∪ 𝐻 ) = ( ( 𝑖 ∪ { 𝑞 } ) ∪ 𝐻 ) )
108 107 eleq1d ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑞 } ) → ( ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ↔ ( ( 𝑖 ∪ { 𝑞 } ) ∪ 𝐻 ) ∈ 𝐼 ) )
109 106 108 anbi12d ⊢ ( 𝑗 = ( 𝑖 ∪ { 𝑞 } ) → ( ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ↔ ( 𝐹 ≈ ( 𝑖 ∪ { 𝑞 } ) ∧ ( ( 𝑖 ∪ { 𝑞 } ) ∪ 𝐻 ) ∈ 𝐼 ) ) )
110 109 rspcev ⊢ ( ( ( 𝑖 ∪ { 𝑞 } ) ∈ 𝒫 𝐺 ∧ ( 𝐹 ≈ ( 𝑖 ∪ { 𝑞 } ) ∧ ( ( 𝑖 ∪ { 𝑞 } ) ∪ 𝐻 ) ∈ 𝐼 ) ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )
111 86 99 105 110 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ∧ ( 𝑖 ∈ 𝒫 ( 𝐺 ∖ { 𝑞 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ≈ 𝑖 ∧ ( 𝑖 ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )
112 75 111 rexlimddv ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )
113 30 112 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) ∧ ( 𝑞 ∈ 𝐺 ∧ ( ¬ 𝑞 ∈ ( 𝐹 ∖ { 𝑟 } ) ∧ ( ( 𝐹 ∖ { 𝑟 } ) ∪ ( 𝐻 ∪ { 𝑞 } ) ) ∈ 𝐼 ) ) ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )
114 29 113 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝐹 ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )
115 114 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) ∧ 𝑟 ∈ 𝐹 ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )
116 21 115 exlimddv ⊢ ( ( 𝜑 ∧ 𝐹 ≠ ∅ ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )
117 19 116 pm2.61dane ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )