This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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