Metamath Proof Explorer

Theorem xpord3inddlem

Description: Induction over the triple Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 2-Feb-2025)

Ref Expression
Hypotheses xpord3.1 ⊢U=xy|x∈A×B×C∧y∈A×B×C∧1st⁡1st⁡xR1st⁡1st⁡y∨1st⁡1st⁡x=1st⁡1st⁡y∧2nd⁡1st⁡xS2nd⁡1st⁡y∨2nd⁡1st⁡x=2nd⁡1st⁡y∧2nd⁡xT2nd⁡y∨2nd⁡x=2nd⁡y∧x≠y
xpord3inddlem.x ⊢κ→X∈A
xpord3inddlem.y ⊢κ→Y∈B
xpord3inddlem.z ⊢κ→Z∈C
xpord3inddlem.1 ⊢κ→RFrA
xpord3inddlem.2 ⊢κ→RPoA
xpord3inddlem.3 ⊢κ→RSeA
xpord3inddlem.4 ⊢κ→SFrB
xpord3inddlem.5 ⊢κ→SPoB
xpord3inddlem.6 ⊢κ→SSeB
xpord3inddlem.7 ⊢κ→TFrC
xpord3inddlem.8 ⊢κ→TPoC
xpord3inddlem.9 ⊢κ→TSeC
xpord3inddlem.10 ⊢a=d→φ↔ψ
xpord3inddlem.11 ⊢b=e→ψ↔χ
xpord3inddlem.12 ⊢c=f→χ↔θ
xpord3inddlem.13 ⊢a=d→τ↔θ
xpord3inddlem.14 ⊢b=e→η↔τ
xpord3inddlem.15 ⊢b=e→ζ↔θ
xpord3inddlem.16 ⊢c=f→σ↔τ
xpord3inddlem.17 ⊢a=X→φ↔ρ
xpord3inddlem.18 ⊢b=Y→ρ↔μ
xpord3inddlem.19 ⊢c=Z→μ↔λ
xpord3inddlem.i ⊢κ∧a∈A∧b∈B∧c∈C→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcθ∧∀d∈PredRAa∀e∈PredSBbχ∧∀d∈PredRAa∀f∈PredTCcζ∧∀d∈PredRAaψ∧∀e∈PredSBb∀f∈PredTCcτ∧∀e∈PredSBbσ∧∀f∈PredTCcη→φ
Assertion xpord3inddlem ⊢κ→λ

Proof

Step Hyp Ref Expression
1 xpord3.1 ⊢U=xy|x∈A×B×C∧y∈A×B×C∧1st⁡1st⁡xR1st⁡1st⁡y∨1st⁡1st⁡x=1st⁡1st⁡y∧2nd⁡1st⁡xS2nd⁡1st⁡y∨2nd⁡1st⁡x=2nd⁡1st⁡y∧2nd⁡xT2nd⁡y∨2nd⁡x=2nd⁡y∧x≠y
2 xpord3inddlem.x ⊢κ→X∈A
3 xpord3inddlem.y ⊢κ→Y∈B
4 xpord3inddlem.z ⊢κ→Z∈C
5 xpord3inddlem.1 ⊢κ→RFrA
6 xpord3inddlem.2 ⊢κ→RPoA
7 xpord3inddlem.3 ⊢κ→RSeA
8 xpord3inddlem.4 ⊢κ→SFrB
9 xpord3inddlem.5 ⊢κ→SPoB
10 xpord3inddlem.6 ⊢κ→SSeB
11 xpord3inddlem.7 ⊢κ→TFrC
12 xpord3inddlem.8 ⊢κ→TPoC
13 xpord3inddlem.9 ⊢κ→TSeC
14 xpord3inddlem.10 ⊢a=d→φ↔ψ
15 xpord3inddlem.11 ⊢b=e→ψ↔χ
16 xpord3inddlem.12 ⊢c=f→χ↔θ
17 xpord3inddlem.13 ⊢a=d→τ↔θ
18 xpord3inddlem.14 ⊢b=e→η↔τ
19 xpord3inddlem.15 ⊢b=e→ζ↔θ
20 xpord3inddlem.16 ⊢c=f→σ↔τ
21 xpord3inddlem.17 ⊢a=X→φ↔ρ
22 xpord3inddlem.18 ⊢b=Y→ρ↔μ
23 xpord3inddlem.19 ⊢c=Z→μ↔λ
24 xpord3inddlem.i ⊢κ∧a∈A∧b∈B∧c∈C→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcθ∧∀d∈PredRAa∀e∈PredSBbχ∧∀d∈PredRAa∀f∈PredTCcζ∧∀d∈PredRAaψ∧∀e∈PredSBb∀f∈PredTCcτ∧∀e∈PredSBbσ∧∀f∈PredTCcη→φ
25 1 5 8 11 frxp3 ⊢κ→UFrA×B×C
26 1 6 9 12 poxp3 ⊢κ→UPoA×B×C
27 1 7 10 13 sexp3 ⊢κ→USeA×B×C
28 bi2.04 ⊢def∈PredUA×B×Cabc→κ→θ↔κ→def∈PredUA×B×Cabc→θ
29 28 3albii ⊢∀d∀e∀fdef∈PredUA×B×Cabc→κ→θ↔∀d∀e∀fκ→def∈PredUA×B×Cabc→θ
30 19.21v ⊢∀fκ→def∈PredUA×B×Cabc→θ↔κ→∀fdef∈PredUA×B×Cabc→θ
31 30 2albii ⊢∀d∀e∀fκ→def∈PredUA×B×Cabc→θ↔∀d∀eκ→∀fdef∈PredUA×B×Cabc→θ
32 19.21v ⊢∀eκ→∀fdef∈PredUA×B×Cabc→θ↔κ→∀e∀fdef∈PredUA×B×Cabc→θ
33 32 albii ⊢∀d∀eκ→∀fdef∈PredUA×B×Cabc→θ↔∀dκ→∀e∀fdef∈PredUA×B×Cabc→θ
34 19.21v ⊢∀dκ→∀e∀fdef∈PredUA×B×Cabc→θ↔κ→∀d∀e∀fdef∈PredUA×B×Cabc→θ
35 33 34 bitri ⊢∀d∀eκ→∀fdef∈PredUA×B×Cabc→θ↔κ→∀d∀e∀fdef∈PredUA×B×Cabc→θ
36 31 35 bitri ⊢∀d∀e∀fκ→def∈PredUA×B×Cabc→θ↔κ→∀d∀e∀fdef∈PredUA×B×Cabc→θ
37 29 36 bitri ⊢∀d∀e∀fdef∈PredUA×B×Cabc→κ→θ↔κ→∀d∀e∀fdef∈PredUA×B×Cabc→θ
38 1 xpord3pred ⊢a∈A∧b∈B∧c∈C→PredUA×B×Cabc=PredRAa∪a×PredSBb∪b×PredTCc∪c∖abc
39 38 adantl ⊢κ∧a∈A∧b∈B∧c∈C→PredUA×B×Cabc=PredRAa∪a×PredSBb∪b×PredTCc∪c∖abc
40 39 eleq2d ⊢κ∧a∈A∧b∈B∧c∈C→def∈PredUA×B×Cabc↔def∈PredRAa∪a×PredSBb∪b×PredTCc∪c∖abc
41 40 imbi1d ⊢κ∧a∈A∧b∈B∧c∈C→def∈PredUA×B×Cabc→θ↔def∈PredRAa∪a×PredSBb∪b×PredTCc∪c∖abc→θ
42 eldifsn ⊢def∈PredRAa∪a×PredSBb∪b×PredTCc∪c∖abc↔def∈PredRAa∪a×PredSBb∪b×PredTCc∪c∧def≠abc
43 otelxp ⊢def∈PredRAa∪a×PredSBb∪b×PredTCc∪c↔d∈PredRAa∪a∧e∈PredSBb∪b∧f∈PredTCc∪c
44 vex ⊢d∈V
45 vex ⊢e∈V
46 vex ⊢f∈V
47 44 45 46 otthne ⊢def≠abc↔d≠a∨e≠b∨f≠c
48 43 47 anbi12i ⊢def∈PredRAa∪a×PredSBb∪b×PredTCc∪c∧def≠abc↔d∈PredRAa∪a∧e∈PredSBb∪b∧f∈PredTCc∪c∧d≠a∨e≠b∨f≠c
49 42 48 bitri ⊢def∈PredRAa∪a×PredSBb∪b×PredTCc∪c∖abc↔d∈PredRAa∪a∧e∈PredSBb∪b∧f∈PredTCc∪c∧d≠a∨e≠b∨f≠c
50 49 imbi1i ⊢def∈PredRAa∪a×PredSBb∪b×PredTCc∪c∖abc→θ↔d∈PredRAa∪a∧e∈PredSBb∪b∧f∈PredTCc∪c∧d≠a∨e≠b∨f≠c→θ
51 41 50 bitrdi ⊢κ∧a∈A∧b∈B∧c∈C→def∈PredUA×B×Cabc→θ↔d∈PredRAa∪a∧e∈PredSBb∪b∧f∈PredTCc∪c∧d≠a∨e≠b∨f≠c→θ
52 impexp ⊢d∈PredRAa∪a∧e∈PredSBb∪b∧f∈PredTCc∪c∧d≠a∨e≠b∨f≠c→θ↔d∈PredRAa∪a∧e∈PredSBb∪b∧f∈PredTCc∪c→d≠a∨e≠b∨f≠c→θ
53 51 52 bitrdi ⊢κ∧a∈A∧b∈B∧c∈C→def∈PredUA×B×Cabc→θ↔d∈PredRAa∪a∧e∈PredSBb∪b∧f∈PredTCc∪c→d≠a∨e≠b∨f≠c→θ
54 53 albidv ⊢κ∧a∈A∧b∈B∧c∈C→∀fdef∈PredUA×B×Cabc→θ↔∀fd∈PredRAa∪a∧e∈PredSBb∪b∧f∈PredTCc∪c→d≠a∨e≠b∨f≠c→θ
55 54 2albidv ⊢κ∧a∈A∧b∈B∧c∈C→∀d∀e∀fdef∈PredUA×B×Cabc→θ↔∀d∀e∀fd∈PredRAa∪a∧e∈PredSBb∪b∧f∈PredTCc∪c→d≠a∨e≠b∨f≠c→θ
56 r3al ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ↔∀d∀e∀fd∈PredRAa∪a∧e∈PredSBb∪b∧f∈PredTCc∪c→d≠a∨e≠b∨f≠c→θ
57 56 bicomi ⊢∀d∀e∀fd∈PredRAa∪a∧e∈PredSBb∪b∧f∈PredTCc∪c→d≠a∨e≠b∨f≠c→θ↔∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ
58 55 57 bitrdi ⊢κ∧a∈A∧b∈B∧c∈C→∀d∀e∀fdef∈PredUA×B×Cabc→θ↔∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ
59 ssun1 ⊢PredTCc⊆PredTCc∪c
60 ssralv ⊢PredTCc⊆PredTCc∪c→∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
61 59 60 ax-mp ⊢∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
62 61 ralimi ⊢∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∪b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
63 ssun1 ⊢PredSBb⊆PredSBb∪b
64 ssralv ⊢PredSBb⊆PredSBb∪b→∀e∈PredSBb∪b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
65 63 64 ax-mp ⊢∀e∈PredSBb∪b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
66 62 65 syl ⊢∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
67 66 ralimi ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∪a∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
68 ssun1 ⊢PredRAa⊆PredRAa∪a
69 ssralv ⊢PredRAa⊆PredRAa∪a→∀d∈PredRAa∪a∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
70 68 69 ax-mp ⊢∀d∈PredRAa∪a∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
71 67 70 syl ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
72 71 adantl ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
73 predpoirr ⊢TPoC→¬c∈PredTCc
74 12 73 syl ⊢κ→¬c∈PredTCc
75 eleq1 ⊢f=c→f∈PredTCc↔c∈PredTCc
76 75 notbid ⊢f=c→¬f∈PredTCc↔¬c∈PredTCc
77 74 76 syl5ibrcom ⊢κ→f=c→¬f∈PredTCc
78 77 necon2ad ⊢κ→f∈PredTCc→f≠c
79 78 imp ⊢κ∧f∈PredTCc→f≠c
80 79 3mix3d ⊢κ∧f∈PredTCc→d≠a∨e≠b∨f≠c
81 pm2.27 ⊢d≠a∨e≠b∨f≠c→d≠a∨e≠b∨f≠c→θ→θ
82 80 81 syl ⊢κ∧f∈PredTCc→d≠a∨e≠b∨f≠c→θ→θ
83 82 ralimdva ⊢κ→∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀f∈PredTCcθ
84 83 ralimdv ⊢κ→∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∀f∈PredTCcθ
85 84 ralimdv ⊢κ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcθ
86 85 adantr ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcθ
87 72 86 mpd ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcθ
88 ssun2 ⊢c⊆PredTCc∪c
89 ssralv ⊢c⊆PredTCc∪c→∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀f∈cd≠a∨e≠b∨f≠c→θ
90 88 89 ax-mp ⊢∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀f∈cd≠a∨e≠b∨f≠c→θ
91 90 ralimi ⊢∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∪b∀f∈cd≠a∨e≠b∨f≠c→θ
92 ssralv ⊢PredSBb⊆PredSBb∪b→∀e∈PredSBb∪b∀f∈cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ
93 63 92 ax-mp ⊢∀e∈PredSBb∪b∀f∈cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ
94 91 93 syl ⊢∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ
95 94 ralimi ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∪a∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ
96 ssralv ⊢PredRAa⊆PredRAa∪a→∀d∈PredRAa∪a∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ
97 68 96 ax-mp ⊢∀d∈PredRAa∪a∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ
98 95 97 syl ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ
99 vex ⊢c∈V
100 biidd ⊢f=c→d≠a↔d≠a
101 biidd ⊢f=c→e≠b↔e≠b
102 neeq1 ⊢f=c→f≠c↔c≠c
103 100 101 102 3orbi123d ⊢f=c→d≠a∨e≠b∨f≠c↔d≠a∨e≠b∨c≠c
104 16 equcoms ⊢f=c→χ↔θ
105 104 bicomd ⊢f=c→θ↔χ
106 103 105 imbi12d ⊢f=c→d≠a∨e≠b∨f≠c→θ↔d≠a∨e≠b∨c≠c→χ
107 99 106 ralsn ⊢∀f∈cd≠a∨e≠b∨f≠c→θ↔d≠a∨e≠b∨c≠c→χ
108 107 2ralbii ⊢∀d∈PredRAa∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ↔∀d∈PredRAa∀e∈PredSBbd≠a∨e≠b∨c≠c→χ
109 98 108 sylib ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBbd≠a∨e≠b∨c≠c→χ
110 109 adantl ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBbd≠a∨e≠b∨c≠c→χ
111 predpoirr ⊢SPoB→¬b∈PredSBb
112 9 111 syl ⊢κ→¬b∈PredSBb
113 eleq1 ⊢e=b→e∈PredSBb↔b∈PredSBb
114 113 notbid ⊢e=b→¬e∈PredSBb↔¬b∈PredSBb
115 112 114 syl5ibrcom ⊢κ→e=b→¬e∈PredSBb
116 115 necon2ad ⊢κ→e∈PredSBb→e≠b
117 116 imp ⊢κ∧e∈PredSBb→e≠b
118 117 3mix2d ⊢κ∧e∈PredSBb→d≠a∨e≠b∨c≠c
119 pm2.27 ⊢d≠a∨e≠b∨c≠c→d≠a∨e≠b∨c≠c→χ→χ
120 118 119 syl ⊢κ∧e∈PredSBb→d≠a∨e≠b∨c≠c→χ→χ
121 120 ralimdva ⊢κ→∀e∈PredSBbd≠a∨e≠b∨c≠c→χ→∀e∈PredSBbχ
122 121 ralimdv ⊢κ→∀d∈PredRAa∀e∈PredSBbd≠a∨e≠b∨c≠c→χ→∀d∈PredRAa∀e∈PredSBbχ
123 122 adantr ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBbd≠a∨e≠b∨c≠c→χ→∀d∈PredRAa∀e∈PredSBbχ
124 110 123 mpd ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBbχ
125 ssun2 ⊢b⊆PredSBb∪b
126 ssralv ⊢b⊆PredSBb∪b→∀e∈PredSBb∪b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
127 125 126 ax-mp ⊢∀e∈PredSBb∪b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
128 62 127 syl ⊢∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
129 128 ralimi ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∪a∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
130 ssralv ⊢PredRAa⊆PredRAa∪a→∀d∈PredRAa∪a∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
131 68 130 ax-mp ⊢∀d∈PredRAa∪a∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
132 129 131 syl ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
133 vex ⊢b∈V
134 biidd ⊢e=b→d≠a↔d≠a
135 neeq1 ⊢e=b→e≠b↔b≠b
136 biidd ⊢e=b→f≠c↔f≠c
137 134 135 136 3orbi123d ⊢e=b→d≠a∨e≠b∨f≠c↔d≠a∨b≠b∨f≠c
138 19 equcoms ⊢e=b→ζ↔θ
139 138 bicomd ⊢e=b→θ↔ζ
140 137 139 imbi12d ⊢e=b→d≠a∨e≠b∨f≠c→θ↔d≠a∨b≠b∨f≠c→ζ
141 140 ralbidv ⊢e=b→∀f∈PredTCcd≠a∨e≠b∨f≠c→θ↔∀f∈PredTCcd≠a∨b≠b∨f≠c→ζ
142 133 141 ralsn ⊢∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ↔∀f∈PredTCcd≠a∨b≠b∨f≠c→ζ
143 142 ralbii ⊢∀d∈PredRAa∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ↔∀d∈PredRAa∀f∈PredTCcd≠a∨b≠b∨f≠c→ζ
144 132 143 sylib ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀f∈PredTCcd≠a∨b≠b∨f≠c→ζ
145 144 adantl ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀f∈PredTCcd≠a∨b≠b∨f≠c→ζ
146 79 3mix3d ⊢κ∧f∈PredTCc→d≠a∨b≠b∨f≠c
147 pm2.27 ⊢d≠a∨b≠b∨f≠c→d≠a∨b≠b∨f≠c→ζ→ζ
148 146 147 syl ⊢κ∧f∈PredTCc→d≠a∨b≠b∨f≠c→ζ→ζ
149 148 ralimdva ⊢κ→∀f∈PredTCcd≠a∨b≠b∨f≠c→ζ→∀f∈PredTCcζ
150 149 ralimdv ⊢κ→∀d∈PredRAa∀f∈PredTCcd≠a∨b≠b∨f≠c→ζ→∀d∈PredRAa∀f∈PredTCcζ
151 150 adantr ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀f∈PredTCcd≠a∨b≠b∨f≠c→ζ→∀d∈PredRAa∀f∈PredTCcζ
152 145 151 mpd ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀f∈PredTCcζ
153 87 124 152 3jca ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcθ∧∀d∈PredRAa∀e∈PredSBbχ∧∀d∈PredRAa∀f∈PredTCcζ
154 ssralv ⊢b⊆PredSBb∪b→∀e∈PredSBb∪b∀f∈cd≠a∨e≠b∨f≠c→θ→∀e∈b∀f∈cd≠a∨e≠b∨f≠c→θ
155 125 154 ax-mp ⊢∀e∈PredSBb∪b∀f∈cd≠a∨e≠b∨f≠c→θ→∀e∈b∀f∈cd≠a∨e≠b∨f≠c→θ
156 91 155 syl ⊢∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈b∀f∈cd≠a∨e≠b∨f≠c→θ
157 156 ralimi ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∪a∀e∈b∀f∈cd≠a∨e≠b∨f≠c→θ
158 ssralv ⊢PredRAa⊆PredRAa∪a→∀d∈PredRAa∪a∀e∈b∀f∈cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈b∀f∈cd≠a∨e≠b∨f≠c→θ
159 68 158 ax-mp ⊢∀d∈PredRAa∪a∀e∈b∀f∈cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈b∀f∈cd≠a∨e≠b∨f≠c→θ
160 157 159 syl ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈b∀f∈cd≠a∨e≠b∨f≠c→θ
161 107 ralbii ⊢∀e∈b∀f∈cd≠a∨e≠b∨f≠c→θ↔∀e∈bd≠a∨e≠b∨c≠c→χ
162 biidd ⊢e=b→c≠c↔c≠c
163 134 135 162 3orbi123d ⊢e=b→d≠a∨e≠b∨c≠c↔d≠a∨b≠b∨c≠c
164 15 equcoms ⊢e=b→ψ↔χ
165 164 bicomd ⊢e=b→χ↔ψ
166 163 165 imbi12d ⊢e=b→d≠a∨e≠b∨c≠c→χ↔d≠a∨b≠b∨c≠c→ψ
167 133 166 ralsn ⊢∀e∈bd≠a∨e≠b∨c≠c→χ↔d≠a∨b≠b∨c≠c→ψ
168 161 167 bitri ⊢∀e∈b∀f∈cd≠a∨e≠b∨f≠c→θ↔d≠a∨b≠b∨c≠c→ψ
169 168 ralbii ⊢∀d∈PredRAa∀e∈b∀f∈cd≠a∨e≠b∨f≠c→θ↔∀d∈PredRAad≠a∨b≠b∨c≠c→ψ
170 160 169 sylib ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAad≠a∨b≠b∨c≠c→ψ
171 170 adantl ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAad≠a∨b≠b∨c≠c→ψ
172 predpoirr ⊢RPoA→¬a∈PredRAa
173 6 172 syl ⊢κ→¬a∈PredRAa
174 eleq1 ⊢d=a→d∈PredRAa↔a∈PredRAa
175 174 notbid ⊢d=a→¬d∈PredRAa↔¬a∈PredRAa
176 173 175 syl5ibrcom ⊢κ→d=a→¬d∈PredRAa
177 176 necon2ad ⊢κ→d∈PredRAa→d≠a
178 177 imp ⊢κ∧d∈PredRAa→d≠a
179 178 3mix1d ⊢κ∧d∈PredRAa→d≠a∨b≠b∨c≠c
180 pm2.27 ⊢d≠a∨b≠b∨c≠c→d≠a∨b≠b∨c≠c→ψ→ψ
181 179 180 syl ⊢κ∧d∈PredRAa→d≠a∨b≠b∨c≠c→ψ→ψ
182 181 ralimdva ⊢κ→∀d∈PredRAad≠a∨b≠b∨c≠c→ψ→∀d∈PredRAaψ
183 182 adantr ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAad≠a∨b≠b∨c≠c→ψ→∀d∈PredRAaψ
184 171 183 mpd ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAaψ
185 ssun2 ⊢a⊆PredRAa∪a
186 ssralv ⊢a⊆PredRAa∪a→∀d∈PredRAa∪a∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀d∈a∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
187 185 186 ax-mp ⊢∀d∈PredRAa∪a∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀d∈a∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
188 67 187 syl ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈a∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
189 vex ⊢a∈V
190 neeq1 ⊢d=a→d≠a↔a≠a
191 biidd ⊢d=a→e≠b↔e≠b
192 biidd ⊢d=a→f≠c↔f≠c
193 190 191 192 3orbi123d ⊢d=a→d≠a∨e≠b∨f≠c↔a≠a∨e≠b∨f≠c
194 17 equcoms ⊢d=a→τ↔θ
195 194 bicomd ⊢d=a→θ↔τ
196 193 195 imbi12d ⊢d=a→d≠a∨e≠b∨f≠c→θ↔a≠a∨e≠b∨f≠c→τ
197 196 2ralbidv ⊢d=a→∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ↔∀e∈PredSBb∀f∈PredTCca≠a∨e≠b∨f≠c→τ
198 189 197 ralsn ⊢∀d∈a∀e∈PredSBb∀f∈PredTCcd≠a∨e≠b∨f≠c→θ↔∀e∈PredSBb∀f∈PredTCca≠a∨e≠b∨f≠c→τ
199 188 198 sylib ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∀f∈PredTCca≠a∨e≠b∨f≠c→τ
200 199 adantl ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∀f∈PredTCca≠a∨e≠b∨f≠c→τ
201 79 3mix3d ⊢κ∧f∈PredTCc→a≠a∨e≠b∨f≠c
202 pm2.27 ⊢a≠a∨e≠b∨f≠c→a≠a∨e≠b∨f≠c→τ→τ
203 201 202 syl ⊢κ∧f∈PredTCc→a≠a∨e≠b∨f≠c→τ→τ
204 203 ralimdva ⊢κ→∀f∈PredTCca≠a∨e≠b∨f≠c→τ→∀f∈PredTCcτ
205 204 ralimdv ⊢κ→∀e∈PredSBb∀f∈PredTCca≠a∨e≠b∨f≠c→τ→∀e∈PredSBb∀f∈PredTCcτ
206 205 adantr ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∀f∈PredTCca≠a∨e≠b∨f≠c→τ→∀e∈PredSBb∀f∈PredTCcτ
207 200 206 mpd ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBb∀f∈PredTCcτ
208 ssralv ⊢a⊆PredRAa∪a→∀d∈PredRAa∪a∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ→∀d∈a∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ
209 185 208 ax-mp ⊢∀d∈PredRAa∪a∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ→∀d∈a∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ
210 95 209 syl ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈a∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ
211 196 2ralbidv ⊢d=a→∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ↔∀e∈PredSBb∀f∈ca≠a∨e≠b∨f≠c→τ
212 189 211 ralsn ⊢∀d∈a∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ↔∀e∈PredSBb∀f∈ca≠a∨e≠b∨f≠c→τ
213 biidd ⊢f=c→a≠a↔a≠a
214 213 101 102 3orbi123d ⊢f=c→a≠a∨e≠b∨f≠c↔a≠a∨e≠b∨c≠c
215 20 bicomd ⊢c=f→τ↔σ
216 215 equcoms ⊢f=c→τ↔σ
217 214 216 imbi12d ⊢f=c→a≠a∨e≠b∨f≠c→τ↔a≠a∨e≠b∨c≠c→σ
218 99 217 ralsn ⊢∀f∈ca≠a∨e≠b∨f≠c→τ↔a≠a∨e≠b∨c≠c→σ
219 218 ralbii ⊢∀e∈PredSBb∀f∈ca≠a∨e≠b∨f≠c→τ↔∀e∈PredSBba≠a∨e≠b∨c≠c→σ
220 212 219 bitri ⊢∀d∈a∀e∈PredSBb∀f∈cd≠a∨e≠b∨f≠c→θ↔∀e∈PredSBba≠a∨e≠b∨c≠c→σ
221 210 220 sylib ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBba≠a∨e≠b∨c≠c→σ
222 221 adantl ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBba≠a∨e≠b∨c≠c→σ
223 117 3mix2d ⊢κ∧e∈PredSBb→a≠a∨e≠b∨c≠c
224 pm2.27 ⊢a≠a∨e≠b∨c≠c→a≠a∨e≠b∨c≠c→σ→σ
225 223 224 syl ⊢κ∧e∈PredSBb→a≠a∨e≠b∨c≠c→σ→σ
226 225 ralimdva ⊢κ→∀e∈PredSBba≠a∨e≠b∨c≠c→σ→∀e∈PredSBbσ
227 226 adantr ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBba≠a∨e≠b∨c≠c→σ→∀e∈PredSBbσ
228 222 227 mpd ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀e∈PredSBbσ
229 184 207 228 3jca ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAaψ∧∀e∈PredSBb∀f∈PredTCcτ∧∀e∈PredSBbσ
230 ssralv ⊢a⊆PredRAa∪a→∀d∈PredRAa∪a∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀d∈a∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
231 185 230 ax-mp ⊢∀d∈PredRAa∪a∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ→∀d∈a∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
232 129 231 syl ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈a∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ
233 196 2ralbidv ⊢d=a→∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ↔∀e∈b∀f∈PredTCca≠a∨e≠b∨f≠c→τ
234 189 233 ralsn ⊢∀d∈a∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ↔∀e∈b∀f∈PredTCca≠a∨e≠b∨f≠c→τ
235 biidd ⊢e=b→a≠a↔a≠a
236 235 135 136 3orbi123d ⊢e=b→a≠a∨e≠b∨f≠c↔a≠a∨b≠b∨f≠c
237 equcomi ⊢e=b→b=e
238 bicom1 ⊢η↔τ→τ↔η
239 237 18 238 3syl ⊢e=b→τ↔η
240 236 239 imbi12d ⊢e=b→a≠a∨e≠b∨f≠c→τ↔a≠a∨b≠b∨f≠c→η
241 240 ralbidv ⊢e=b→∀f∈PredTCca≠a∨e≠b∨f≠c→τ↔∀f∈PredTCca≠a∨b≠b∨f≠c→η
242 133 241 ralsn ⊢∀e∈b∀f∈PredTCca≠a∨e≠b∨f≠c→τ↔∀f∈PredTCca≠a∨b≠b∨f≠c→η
243 234 242 bitri ⊢∀d∈a∀e∈b∀f∈PredTCcd≠a∨e≠b∨f≠c→θ↔∀f∈PredTCca≠a∨b≠b∨f≠c→η
244 232 243 sylib ⊢∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀f∈PredTCca≠a∨b≠b∨f≠c→η
245 244 adantl ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀f∈PredTCca≠a∨b≠b∨f≠c→η
246 79 3mix3d ⊢κ∧f∈PredTCc→a≠a∨b≠b∨f≠c
247 pm2.27 ⊢a≠a∨b≠b∨f≠c→a≠a∨b≠b∨f≠c→η→η
248 246 247 syl ⊢κ∧f∈PredTCc→a≠a∨b≠b∨f≠c→η→η
249 248 ralimdva ⊢κ→∀f∈PredTCca≠a∨b≠b∨f≠c→η→∀f∈PredTCcη
250 249 adantr ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀f∈PredTCca≠a∨b≠b∨f≠c→η→∀f∈PredTCcη
251 245 250 mpd ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀f∈PredTCcη
252 153 229 251 3jca ⊢κ∧∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcθ∧∀d∈PredRAa∀e∈PredSBbχ∧∀d∈PredRAa∀f∈PredTCcζ∧∀d∈PredRAaψ∧∀e∈PredSBb∀f∈PredTCcτ∧∀e∈PredSBbσ∧∀f∈PredTCcη
253 252 ex ⊢κ→∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcθ∧∀d∈PredRAa∀e∈PredSBbχ∧∀d∈PredRAa∀f∈PredTCcζ∧∀d∈PredRAaψ∧∀e∈PredSBb∀f∈PredTCcτ∧∀e∈PredSBbσ∧∀f∈PredTCcη
254 253 adantr ⊢κ∧a∈A∧b∈B∧c∈C→∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→∀d∈PredRAa∀e∈PredSBb∀f∈PredTCcθ∧∀d∈PredRAa∀e∈PredSBbχ∧∀d∈PredRAa∀f∈PredTCcζ∧∀d∈PredRAaψ∧∀e∈PredSBb∀f∈PredTCcτ∧∀e∈PredSBbσ∧∀f∈PredTCcη
255 254 24 syld ⊢κ∧a∈A∧b∈B∧c∈C→∀d∈PredRAa∪a∀e∈PredSBb∪b∀f∈PredTCc∪cd≠a∨e≠b∨f≠c→θ→φ
256 58 255 sylbid ⊢κ∧a∈A∧b∈B∧c∈C→∀d∀e∀fdef∈PredUA×B×Cabc→θ→φ
257 256 expcom ⊢a∈A∧b∈B∧c∈C→κ→∀d∀e∀fdef∈PredUA×B×Cabc→θ→φ
258 257 a2d ⊢a∈A∧b∈B∧c∈C→κ→∀d∀e∀fdef∈PredUA×B×Cabc→θ→κ→φ
259 37 258 biimtrid ⊢a∈A∧b∈B∧c∈C→∀d∀e∀fdef∈PredUA×B×Cabc→κ→θ→κ→φ
260 14 imbi2d ⊢a=d→κ→φ↔κ→ψ
261 15 imbi2d ⊢b=e→κ→ψ↔κ→χ
262 16 imbi2d ⊢c=f→κ→χ↔κ→θ
263 21 imbi2d ⊢a=X→κ→φ↔κ→ρ
264 22 imbi2d ⊢b=Y→κ→ρ↔κ→μ
265 23 imbi2d ⊢c=Z→κ→μ↔κ→λ
266 259 260 261 262 263 264 265 frpoins3xp3g ⊢UFrA×B×C∧UPoA×B×C∧USeA×B×C∧X∈A∧Y∈B∧Z∈C→κ→λ
267 25 26 27 2 3 4 266 syl33anc ⊢κ→κ→λ
268 267 pm2.43i ⊢κ→λ