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

Metamath Proof Explorer

Theorem mreexexlemd

Description: This lemma is used to generate substitution instances of the induction hypothesis in mreexexd . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mreexexlemd.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
mreexexlemd.2 ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑋 ∖ 𝐻 ) )
mreexexlemd.3 ⊢ ( 𝜑 → 𝐺 ⊆ ( 𝑋 ∖ 𝐻 ) )
mreexexlemd.4 ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
mreexexlemd.5 ⊢ ( 𝜑 → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
mreexexlemd.6 ⊢ ( 𝜑 → ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) )
mreexexlemd.7 ⊢ ( 𝜑 → ∀ 𝑡 ∀ 𝑢 ∈ 𝒫 ( 𝑋 ∖ 𝑡 ) ∀ 𝑣 ∈ 𝒫 ( 𝑋 ∖ 𝑡 ) ( ( ( 𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾 ) ∧ 𝑢 ⊆ ( 𝑁 ‘ ( 𝑣 ∪ 𝑡 ) ) ∧ ( 𝑢 ∪ 𝑡 ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑣 ( 𝑢 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝑡 ) ∈ 𝐼 ) ) )
Assertion mreexexlemd ( 𝜑 → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 mreexexlemd.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
2 mreexexlemd.2 ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑋 ∖ 𝐻 ) )
3 mreexexlemd.3 ⊢ ( 𝜑 → 𝐺 ⊆ ( 𝑋 ∖ 𝐻 ) )
4 mreexexlemd.4 ⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
5 mreexexlemd.5 ⊢ ( 𝜑 → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
6 mreexexlemd.6 ⊢ ( 𝜑 → ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) )
7 mreexexlemd.7 ⊢ ( 𝜑 → ∀ 𝑡 ∀ 𝑢 ∈ 𝒫 ( 𝑋 ∖ 𝑡 ) ∀ 𝑣 ∈ 𝒫 ( 𝑋 ∖ 𝑡 ) ( ( ( 𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾 ) ∧ 𝑢 ⊆ ( 𝑁 ‘ ( 𝑣 ∪ 𝑡 ) ) ∧ ( 𝑢 ∪ 𝑡 ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑣 ( 𝑢 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝑡 ) ∈ 𝐼 ) ) )
8 simplr ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → 𝑢 = 𝑓 )
9 8 breq1d ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → ( 𝑢 ≈ 𝐾 ↔ 𝑓 ≈ 𝐾 ) )
10 simpr ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → 𝑣 = 𝑔 )
11 10 breq1d ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → ( 𝑣 ≈ 𝐾 ↔ 𝑔 ≈ 𝐾 ) )
12 9 11 orbi12d ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → ( ( 𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾 ) ↔ ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ) )
13 simpll ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → 𝑡 = ℎ )
14 10 13 uneq12d ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → ( 𝑣 ∪ 𝑡 ) = ( 𝑔 ∪ ℎ ) )
15 14 fveq2d ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → ( 𝑁 ‘ ( 𝑣 ∪ 𝑡 ) ) = ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) )
16 8 15 sseq12d ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → ( 𝑢 ⊆ ( 𝑁 ‘ ( 𝑣 ∪ 𝑡 ) ) ↔ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ) )
17 8 13 uneq12d ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → ( 𝑢 ∪ 𝑡 ) = ( 𝑓 ∪ ℎ ) )
18 17 eleq1d ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → ( ( 𝑢 ∪ 𝑡 ) ∈ 𝐼 ↔ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) )
19 12 16 18 3anbi123d ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → ( ( ( 𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾 ) ∧ 𝑢 ⊆ ( 𝑁 ‘ ( 𝑣 ∪ 𝑡 ) ) ∧ ( 𝑢 ∪ 𝑡 ) ∈ 𝐼 ) ↔ ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ) )
20 simpllr ⊢ ( ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) ∧ 𝑖 = 𝑗 ) → 𝑢 = 𝑓 )
21 simpr ⊢ ( ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) ∧ 𝑖 = 𝑗 ) → 𝑖 = 𝑗 )
22 20 21 breq12d ⊢ ( ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) ∧ 𝑖 = 𝑗 ) → ( 𝑢 ≈ 𝑖 ↔ 𝑓 ≈ 𝑗 ) )
23 simplll ⊢ ( ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) ∧ 𝑖 = 𝑗 ) → 𝑡 = ℎ )
24 21 23 uneq12d ⊢ ( ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) ∧ 𝑖 = 𝑗 ) → ( 𝑖 ∪ 𝑡 ) = ( 𝑗 ∪ ℎ ) )
25 24 eleq1d ⊢ ( ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) ∧ 𝑖 = 𝑗 ) → ( ( 𝑖 ∪ 𝑡 ) ∈ 𝐼 ↔ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) )
26 22 25 anbi12d ⊢ ( ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) ∧ 𝑖 = 𝑗 ) → ( ( 𝑢 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝑡 ) ∈ 𝐼 ) ↔ ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) )
27 simplr ⊢ ( ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) ∧ 𝑖 = 𝑗 ) → 𝑣 = 𝑔 )
28 27 pweqd ⊢ ( ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) ∧ 𝑖 = 𝑗 ) → 𝒫 𝑣 = 𝒫 𝑔 )
29 26 28 cbvrexdva2 ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → ( ∃ 𝑖 ∈ 𝒫 𝑣 ( 𝑢 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝑡 ) ∈ 𝐼 ) ↔ ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) )
30 19 29 imbi12d ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → ( ( ( ( 𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾 ) ∧ 𝑢 ⊆ ( 𝑁 ‘ ( 𝑣 ∪ 𝑡 ) ) ∧ ( 𝑢 ∪ 𝑡 ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑣 ( 𝑢 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝑡 ) ∈ 𝐼 ) ) ↔ ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) ) )
31 simpl ⊢ ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) → 𝑡 = ℎ )
32 31 difeq2d ⊢ ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) → ( 𝑋 ∖ 𝑡 ) = ( 𝑋 ∖ ℎ ) )
33 32 pweqd ⊢ ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) → 𝒫 ( 𝑋 ∖ 𝑡 ) = 𝒫 ( 𝑋 ∖ ℎ ) )
34 33 adantr ⊢ ( ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) ∧ 𝑣 = 𝑔 ) → 𝒫 ( 𝑋 ∖ 𝑡 ) = 𝒫 ( 𝑋 ∖ ℎ ) )
35 30 34 cbvraldva2 ⊢ ( ( 𝑡 = ℎ ∧ 𝑢 = 𝑓 ) → ( ∀ 𝑣 ∈ 𝒫 ( 𝑋 ∖ 𝑡 ) ( ( ( 𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾 ) ∧ 𝑢 ⊆ ( 𝑁 ‘ ( 𝑣 ∪ 𝑡 ) ) ∧ ( 𝑢 ∪ 𝑡 ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑣 ( 𝑢 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝑡 ) ∈ 𝐼 ) ) ↔ ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) ) )
36 35 33 cbvraldva2 ⊢ ( 𝑡 = ℎ → ( ∀ 𝑢 ∈ 𝒫 ( 𝑋 ∖ 𝑡 ) ∀ 𝑣 ∈ 𝒫 ( 𝑋 ∖ 𝑡 ) ( ( ( 𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾 ) ∧ 𝑢 ⊆ ( 𝑁 ‘ ( 𝑣 ∪ 𝑡 ) ) ∧ ( 𝑢 ∪ 𝑡 ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑣 ( 𝑢 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝑡 ) ∈ 𝐼 ) ) ↔ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) ) )
37 36 cbvalvw ⊢ ( ∀ 𝑡 ∀ 𝑢 ∈ 𝒫 ( 𝑋 ∖ 𝑡 ) ∀ 𝑣 ∈ 𝒫 ( 𝑋 ∖ 𝑡 ) ( ( ( 𝑢 ≈ 𝐾 ∨ 𝑣 ≈ 𝐾 ) ∧ 𝑢 ⊆ ( 𝑁 ‘ ( 𝑣 ∪ 𝑡 ) ) ∧ ( 𝑢 ∪ 𝑡 ) ∈ 𝐼 ) → ∃ 𝑖 ∈ 𝒫 𝑣 ( 𝑢 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝑡 ) ∈ 𝐼 ) ) ↔ ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) )
38 7 37 sylib ⊢ ( 𝜑 → ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) )
39 ssun2 ⊢ 𝐻 ⊆ ( 𝐹 ∪ 𝐻 )
40 39 a1i ⊢ ( 𝜑 → 𝐻 ⊆ ( 𝐹 ∪ 𝐻 ) )
41 5 40 ssexd ⊢ ( 𝜑 → 𝐻 ∈ V )
42 1 difexd ⊢ ( 𝜑 → ( 𝑋 ∖ 𝐻 ) ∈ V )
43 42 2 sselpwd ⊢ ( 𝜑 → 𝐹 ∈ 𝒫 ( 𝑋 ∖ 𝐻 ) )
44 43 adantr ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → 𝐹 ∈ 𝒫 ( 𝑋 ∖ 𝐻 ) )
45 simpr ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ℎ = 𝐻 )
46 45 difeq2d ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ( 𝑋 ∖ ℎ ) = ( 𝑋 ∖ 𝐻 ) )
47 46 pweqd ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → 𝒫 ( 𝑋 ∖ ℎ ) = 𝒫 ( 𝑋 ∖ 𝐻 ) )
48 44 47 eleqtrrd ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → 𝐹 ∈ 𝒫 ( 𝑋 ∖ ℎ ) )
49 42 3 sselpwd ⊢ ( 𝜑 → 𝐺 ∈ 𝒫 ( 𝑋 ∖ 𝐻 ) )
50 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) → 𝐺 ∈ 𝒫 ( 𝑋 ∖ 𝐻 ) )
51 47 adantr ⊢ ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) → 𝒫 ( 𝑋 ∖ ℎ ) = 𝒫 ( 𝑋 ∖ 𝐻 ) )
52 50 51 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) → 𝐺 ∈ 𝒫 ( 𝑋 ∖ ℎ ) )
53 simplr ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
54 53 breq1d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑓 ≈ 𝐾 ↔ 𝐹 ≈ 𝐾 ) )
55 simpr ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
56 55 breq1d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑔 ≈ 𝐾 ↔ 𝐺 ≈ 𝐾 ) )
57 54 56 orbi12d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ↔ ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ) )
58 simpllr ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ℎ = 𝐻 )
59 55 58 uneq12d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑔 ∪ ℎ ) = ( 𝐺 ∪ 𝐻 ) )
60 59 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) = ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
61 53 60 sseq12d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ↔ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ) )
62 53 58 uneq12d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑓 ∪ ℎ ) = ( 𝐹 ∪ 𝐻 ) )
63 62 eleq1d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ∪ ℎ ) ∈ 𝐼 ↔ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) )
64 57 61 63 3anbi123d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ↔ ( ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ∧ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) ) )
65 55 pweqd ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝒫 𝑔 = 𝒫 𝐺 )
66 53 breq1d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑓 ≈ 𝑗 ↔ 𝐹 ≈ 𝑗 ) )
67 58 uneq2d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑗 ∪ ℎ ) = ( 𝑗 ∪ 𝐻 ) )
68 67 eleq1d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑗 ∪ ℎ ) ∈ 𝐼 ↔ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )
69 66 68 anbi12d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ↔ ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) )
70 65 69 rexeqbidv ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ↔ ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) )
71 64 70 imbi12d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ( ( ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ∧ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) ) )
72 52 71 rspcdv ⊢ ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) → ( ( ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ∧ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) ) )
73 48 72 rspcimdv ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ( ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) → ( ( ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ∧ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) ) )
74 41 73 spcimdv ⊢ ( 𝜑 → ( ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) → ( ( ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ∧ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) ) )
75 38 74 mpd ⊢ ( 𝜑 → ( ( ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ∧ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) )
76 6 4 5 75 mp3and ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )