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 difexg ⊢ ( 𝑋 ∈ 𝐽 → ( 𝑋 ∖ 𝐻 ) ∈ V )
43 1 42 syl ⊢ ( 𝜑 → ( 𝑋 ∖ 𝐻 ) ∈ V )
44 43 2 sselpwd ⊢ ( 𝜑 → 𝐹 ∈ 𝒫 ( 𝑋 ∖ 𝐻 ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → 𝐹 ∈ 𝒫 ( 𝑋 ∖ 𝐻 ) )
46 simpr ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ℎ = 𝐻 )
47 46 difeq2d ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ( 𝑋 ∖ ℎ ) = ( 𝑋 ∖ 𝐻 ) )
48 47 pweqd ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → 𝒫 ( 𝑋 ∖ ℎ ) = 𝒫 ( 𝑋 ∖ 𝐻 ) )
49 45 48 eleqtrrd ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → 𝐹 ∈ 𝒫 ( 𝑋 ∖ ℎ ) )
50 43 3 sselpwd ⊢ ( 𝜑 → 𝐺 ∈ 𝒫 ( 𝑋 ∖ 𝐻 ) )
51 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) → 𝐺 ∈ 𝒫 ( 𝑋 ∖ 𝐻 ) )
52 48 adantr ⊢ ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) → 𝒫 ( 𝑋 ∖ ℎ ) = 𝒫 ( 𝑋 ∖ 𝐻 ) )
53 51 52 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) → 𝐺 ∈ 𝒫 ( 𝑋 ∖ ℎ ) )
54 simplr ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
55 54 breq1d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑓 ≈ 𝐾 ↔ 𝐹 ≈ 𝐾 ) )
56 simpr ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
57 56 breq1d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑔 ≈ 𝐾 ↔ 𝐺 ≈ 𝐾 ) )
58 55 57 orbi12d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ↔ ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ) )
59 simpllr ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ℎ = 𝐻 )
60 56 59 uneq12d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑔 ∪ ℎ ) = ( 𝐺 ∪ 𝐻 ) )
61 60 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) = ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
62 54 61 sseq12d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ↔ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ) )
63 54 59 uneq12d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑓 ∪ ℎ ) = ( 𝐹 ∪ 𝐻 ) )
64 63 eleq1d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ∪ ℎ ) ∈ 𝐼 ↔ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) )
65 58 62 64 3anbi123d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) ↔ ( ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ∧ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) ) )
66 56 pweqd ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → 𝒫 𝑔 = 𝒫 𝐺 )
67 54 breq1d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑓 ≈ 𝑗 ↔ 𝐹 ≈ 𝑗 ) )
68 59 uneq2d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( 𝑗 ∪ ℎ ) = ( 𝑗 ∪ 𝐻 ) )
69 68 eleq1d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑗 ∪ ℎ ) ∈ 𝐼 ↔ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )
70 67 69 anbi12d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ↔ ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) )
71 66 70 rexeqbidv ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ↔ ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) )
72 65 71 imbi12d ⊢ ( ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) ∧ 𝑔 = 𝐺 ) → ( ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) ↔ ( ( ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ∧ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) ) )
73 53 72 rspcdv ⊢ ( ( ( 𝜑 ∧ ℎ = 𝐻 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) → ( ( ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ∧ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) ) )
74 49 73 rspcimdv ⊢ ( ( 𝜑 ∧ ℎ = 𝐻 ) → ( ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) → ( ( ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ∧ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) ) )
75 41 74 spcimdv ⊢ ( 𝜑 → ( ∀ ℎ ∀ 𝑓 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ∀ 𝑔 ∈ 𝒫 ( 𝑋 ∖ ℎ ) ( ( ( 𝑓 ≈ 𝐾 ∨ 𝑔 ≈ 𝐾 ) ∧ 𝑓 ⊆ ( 𝑁 ‘ ( 𝑔 ∪ ℎ ) ) ∧ ( 𝑓 ∪ ℎ ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝑔 ( 𝑓 ≈ 𝑗 ∧ ( 𝑗 ∪ ℎ ) ∈ 𝐼 ) ) → ( ( ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ∧ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) ) )
76 38 75 mpd ⊢ ( 𝜑 → ( ( ( 𝐹 ≈ 𝐾 ∨ 𝐺 ≈ 𝐾 ) ∧ 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) ) )
77 6 4 5 76 mp3and ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑗 ∧ ( 𝑗 ∪ 𝐻 ) ∈ 𝐼 ) )