Metamath Proof Explorer

Theorem ordtbas2

Description: Lemma for ordtbas . (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses ordtval.1 ⊢ 𝑋 = dom 𝑅
ordtval.2 ⊢ 𝐴 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
ordtval.3 ⊢ 𝐵 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
ordtval.4 ⊢ 𝐶 = ran ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } )
Assertion ordtbas2 ( 𝑅 ∈ TosetRel → ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ordtval.1 ⊢ 𝑋 = dom 𝑅
2 ordtval.2 ⊢ 𝐴 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
3 ordtval.3 ⊢ 𝐵 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
4 ordtval.4 ⊢ 𝐶 = ran ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } )
5 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
6 ssun2 ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) )
7 1 2 3 ordtuni ⊢ ( 𝑅 ∈ TosetRel → 𝑋 = ∪ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) )
8 dmexg ⊢ ( 𝑅 ∈ TosetRel → dom 𝑅 ∈ V )
9 1 8 eqeltrid ⊢ ( 𝑅 ∈ TosetRel → 𝑋 ∈ V )
10 7 9 eqeltrrd ⊢ ( 𝑅 ∈ TosetRel → ∪ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
11 uniexb ⊢ ( ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ V ↔ ∪ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
12 10 11 sylibr ⊢ ( 𝑅 ∈ TosetRel → ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ V )
13 ssexg ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∧ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) ∈ V ) → ( 𝐴 ∪ 𝐵 ) ∈ V )
14 6 12 13 sylancr ⊢ ( 𝑅 ∈ TosetRel → ( 𝐴 ∪ 𝐵 ) ∈ V )
15 ssexg ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → 𝐴 ∈ V )
16 5 14 15 sylancr ⊢ ( 𝑅 ∈ TosetRel → 𝐴 ∈ V )
17 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
18 ssexg ⊢ ( ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ∈ V ) → 𝐵 ∈ V )
19 17 14 18 sylancr ⊢ ( 𝑅 ∈ TosetRel → 𝐵 ∈ V )
20 elfiun ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑧 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ ( 𝑧 ∈ ( fi ‘ 𝐴 ) ∨ 𝑧 ∈ ( fi ‘ 𝐵 ) ∨ ∃ 𝑚 ∈ ( fi ‘ 𝐴 ) ∃ 𝑛 ∈ ( fi ‘ 𝐵 ) 𝑧 = ( 𝑚 ∩ 𝑛 ) ) ) )
21 16 19 20 syl2anc ⊢ ( 𝑅 ∈ TosetRel → ( 𝑧 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ ( 𝑧 ∈ ( fi ‘ 𝐴 ) ∨ 𝑧 ∈ ( fi ‘ 𝐵 ) ∨ ∃ 𝑚 ∈ ( fi ‘ 𝐴 ) ∃ 𝑛 ∈ ( fi ‘ 𝐵 ) 𝑧 = ( 𝑚 ∩ 𝑛 ) ) ) )
22 1 2 ordtbaslem ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ 𝐴 ) = 𝐴 )
23 22 5 eqsstrdi ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ 𝐴 ) ⊆ ( 𝐴 ∪ 𝐵 ) )
24 ssun1 ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 )
25 23 24 sstrdi ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ 𝐴 ) ⊆ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
26 25 sseld ⊢ ( 𝑅 ∈ TosetRel → ( 𝑧 ∈ ( fi ‘ 𝐴 ) → 𝑧 ∈ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
27 cnvtsr ⊢ ( 𝑅 ∈ TosetRel → ◡ 𝑅 ∈ TosetRel )
28 df-rn ⊢ ran 𝑅 = dom ◡ 𝑅
29 eqid ⊢ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) = ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } )
30 28 29 ordtbaslem ⊢ ( ◡ 𝑅 ∈ TosetRel → ( fi ‘ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ) = ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) )
31 27 30 syl ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ) = ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) )
32 tsrps ⊢ ( 𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel )
33 1 psrn ⊢ ( 𝑅 ∈ PosetRel → 𝑋 = ran 𝑅 )
34 32 33 syl ⊢ ( 𝑅 ∈ TosetRel → 𝑋 = ran 𝑅 )
35 vex ⊢ 𝑦 ∈ V
36 vex ⊢ 𝑥 ∈ V
37 35 36 brcnv ⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
38 37 bicomi ⊢ ( 𝑥 𝑅 𝑦 ↔ 𝑦 ◡ 𝑅 𝑥 )
39 38 notbii ⊢ ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 ◡ 𝑅 𝑥 )
40 39 a1i ⊢ ( 𝑅 ∈ TosetRel → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑦 ◡ 𝑅 𝑥 ) )
41 34 40 rabeqbidv ⊢ ( 𝑅 ∈ TosetRel → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } = { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } )
42 34 41 mpteq12dv ⊢ ( 𝑅 ∈ TosetRel → ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) = ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) )
43 42 rneqd ⊢ ( 𝑅 ∈ TosetRel → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) = ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) )
44 3 43 syl5eq ⊢ ( 𝑅 ∈ TosetRel → 𝐵 = ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) )
45 44 fveq2d ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ 𝐵 ) = ( fi ‘ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ) )
46 31 45 44 3eqtr4d ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ 𝐵 ) = 𝐵 )
47 46 17 eqsstrdi ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ 𝐵 ) ⊆ ( 𝐴 ∪ 𝐵 ) )
48 47 24 sstrdi ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ 𝐵 ) ⊆ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
49 48 sseld ⊢ ( 𝑅 ∈ TosetRel → ( 𝑧 ∈ ( fi ‘ 𝐵 ) → 𝑧 ∈ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
50 ssun2 ⊢ 𝐶 ⊆ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 )
51 22 2 eqtrdi ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ 𝐴 ) = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
52 51 eleq2d ⊢ ( 𝑅 ∈ TosetRel → ( 𝑚 ∈ ( fi ‘ 𝐴 ) ↔ 𝑚 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) )
53 breq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝑎 ) )
54 53 notbid ⊢ ( 𝑥 = 𝑎 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝑎 ) )
55 54 rabbidv ⊢ ( 𝑥 = 𝑎 → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } )
56 55 cbvmptv ⊢ ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) = ( 𝑎 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } )
57 56 elrnmpt ⊢ ( 𝑚 ∈ V → ( 𝑚 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ↔ ∃ 𝑎 ∈ 𝑋 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ) )
58 57 elv ⊢ ( 𝑚 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ↔ ∃ 𝑎 ∈ 𝑋 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } )
59 52 58 bitrdi ⊢ ( 𝑅 ∈ TosetRel → ( 𝑚 ∈ ( fi ‘ 𝐴 ) ↔ ∃ 𝑎 ∈ 𝑋 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ) )
60 46 3 eqtrdi ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ 𝐵 ) = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
61 60 eleq2d ⊢ ( 𝑅 ∈ TosetRel → ( 𝑛 ∈ ( fi ‘ 𝐵 ) ↔ 𝑛 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) )
62 breq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 𝑅 𝑦 ↔ 𝑏 𝑅 𝑦 ) )
63 62 notbid ⊢ ( 𝑥 = 𝑏 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑏 𝑅 𝑦 ) )
64 63 rabbidv ⊢ ( 𝑥 = 𝑏 → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } )
65 64 cbvmptv ⊢ ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) = ( 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } )
66 65 elrnmpt ⊢ ( 𝑛 ∈ V → ( 𝑛 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ↔ ∃ 𝑏 ∈ 𝑋 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) )
67 66 elv ⊢ ( 𝑛 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ↔ ∃ 𝑏 ∈ 𝑋 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } )
68 61 67 bitrdi ⊢ ( 𝑅 ∈ TosetRel → ( 𝑛 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑏 ∈ 𝑋 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) )
69 59 68 anbi12d ⊢ ( 𝑅 ∈ TosetRel → ( ( 𝑚 ∈ ( fi ‘ 𝐴 ) ∧ 𝑛 ∈ ( fi ‘ 𝐵 ) ) ↔ ( ∃ 𝑎 ∈ 𝑋 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∧ ∃ 𝑏 ∈ 𝑋 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) ) )
70 reeanv ⊢ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∧ 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) ↔ ( ∃ 𝑎 ∈ 𝑋 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∧ ∃ 𝑏 ∈ 𝑋 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) )
71 ineq12 ⊢ ( ( 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∧ 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) → ( 𝑚 ∩ 𝑛 ) = ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) )
72 inrab ⊢ ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) }
73 71 72 eqtrdi ⊢ ( ( 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∧ 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) → ( 𝑚 ∩ 𝑛 ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } )
74 73 reximi ⊢ ( ∃ 𝑏 ∈ 𝑋 ( 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∧ 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) → ∃ 𝑏 ∈ 𝑋 ( 𝑚 ∩ 𝑛 ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } )
75 74 reximi ⊢ ( ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∧ 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑚 ∩ 𝑛 ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } )
76 70 75 sylbir ⊢ ( ( ∃ 𝑎 ∈ 𝑋 𝑚 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∧ ∃ 𝑏 ∈ 𝑋 𝑛 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑚 ∩ 𝑛 ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } )
77 69 76 syl6bi ⊢ ( 𝑅 ∈ TosetRel → ( ( 𝑚 ∈ ( fi ‘ 𝐴 ) ∧ 𝑛 ∈ ( fi ‘ 𝐵 ) ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑚 ∩ 𝑛 ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } ) )
78 77 imp ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ 𝐴 ) ∧ 𝑛 ∈ ( fi ‘ 𝐵 ) ) ) → ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑚 ∩ 𝑛 ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } )
79 vex ⊢ 𝑚 ∈ V
80 79 inex1 ⊢ ( 𝑚 ∩ 𝑛 ) ∈ V
81 eqid ⊢ ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } ) = ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } )
82 81 elrnmpog ⊢ ( ( 𝑚 ∩ 𝑛 ) ∈ V → ( ( 𝑚 ∩ 𝑛 ) ∈ ran ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } ) ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑚 ∩ 𝑛 ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } ) )
83 80 82 ax-mp ⊢ ( ( 𝑚 ∩ 𝑛 ) ∈ ran ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } ) ↔ ∃ 𝑎 ∈ 𝑋 ∃ 𝑏 ∈ 𝑋 ( 𝑚 ∩ 𝑛 ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } )
84 78 83 sylibr ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ 𝐴 ) ∧ 𝑛 ∈ ( fi ‘ 𝐵 ) ) ) → ( 𝑚 ∩ 𝑛 ) ∈ ran ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } ) )
85 84 4 eleqtrrdi ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ 𝐴 ) ∧ 𝑛 ∈ ( fi ‘ 𝐵 ) ) ) → ( 𝑚 ∩ 𝑛 ) ∈ 𝐶 )
86 50 85 sseldi ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ 𝐴 ) ∧ 𝑛 ∈ ( fi ‘ 𝐵 ) ) ) → ( 𝑚 ∩ 𝑛 ) ∈ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
87 eleq1 ⊢ ( 𝑧 = ( 𝑚 ∩ 𝑛 ) → ( 𝑧 ∈ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ↔ ( 𝑚 ∩ 𝑛 ) ∈ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
88 86 87 syl5ibrcom ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑚 ∈ ( fi ‘ 𝐴 ) ∧ 𝑛 ∈ ( fi ‘ 𝐵 ) ) ) → ( 𝑧 = ( 𝑚 ∩ 𝑛 ) → 𝑧 ∈ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
89 88 rexlimdvva ⊢ ( 𝑅 ∈ TosetRel → ( ∃ 𝑚 ∈ ( fi ‘ 𝐴 ) ∃ 𝑛 ∈ ( fi ‘ 𝐵 ) 𝑧 = ( 𝑚 ∩ 𝑛 ) → 𝑧 ∈ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
90 26 49 89 3jaod ⊢ ( 𝑅 ∈ TosetRel → ( ( 𝑧 ∈ ( fi ‘ 𝐴 ) ∨ 𝑧 ∈ ( fi ‘ 𝐵 ) ∨ ∃ 𝑚 ∈ ( fi ‘ 𝐴 ) ∃ 𝑛 ∈ ( fi ‘ 𝐵 ) 𝑧 = ( 𝑚 ∩ 𝑛 ) ) → 𝑧 ∈ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
91 21 90 sylbid ⊢ ( 𝑅 ∈ TosetRel → ( 𝑧 ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) → 𝑧 ∈ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ) )
92 91 ssrdv ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ⊆ ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )
93 ssfii ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ V → ( 𝐴 ∪ 𝐵 ) ⊆ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
94 14 93 syl ⊢ ( 𝑅 ∈ TosetRel → ( 𝐴 ∪ 𝐵 ) ⊆ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
95 94 adantr ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝐴 ∪ 𝐵 ) ⊆ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
96 simprl ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑎 ∈ 𝑋 )
97 eqidd ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } )
98 55 rspceeqv ⊢ ( ( 𝑎 ∈ 𝑋 ∧ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ) → ∃ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
99 96 97 98 syl2anc ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ∃ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
100 9 adantr ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑋 ∈ V )
101 rabexg ⊢ ( 𝑋 ∈ V → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ V )
102 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
103 102 elrnmpt ⊢ ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ V → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
104 100 101 103 3syl ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ↔ ∃ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
105 99 104 mpbird ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
106 105 2 eleqtrrdi ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ 𝐴 )
107 5 106 sseldi ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ ( 𝐴 ∪ 𝐵 ) )
108 95 107 sseldd ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
109 simprr ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑏 ∈ 𝑋 )
110 eqidd ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } )
111 64 rspceeqv ⊢ ( ( 𝑏 ∈ 𝑋 ∧ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) → ∃ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
112 109 110 111 syl2anc ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ∃ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
113 rabexg ⊢ ( 𝑋 ∈ V → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ∈ V )
114 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
115 114 elrnmpt ⊢ ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ∈ V → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ↔ ∃ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
116 100 113 115 3syl ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ↔ ∃ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
117 112 116 mpbird ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
118 117 3 eleqtrrdi ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ∈ 𝐵 )
119 17 118 sseldi ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ∈ ( 𝐴 ∪ 𝐵 ) )
120 95 119 sseldd ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
121 fiin ⊢ ( ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ∧ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
122 108 120 121 syl2anc ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑏 𝑅 𝑦 } ) ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
123 72 122 eqeltrrid ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
124 123 ralrimivva ⊢ ( 𝑅 ∈ TosetRel → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
125 81 fmpo ⊢ ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } ∈ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } ) : ( 𝑋 × 𝑋 ) ⟶ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
126 124 125 sylib ⊢ ( 𝑅 ∈ TosetRel → ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } ) : ( 𝑋 × 𝑋 ) ⟶ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
127 126 frnd ⊢ ( 𝑅 ∈ TosetRel → ran ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑏 𝑅 𝑦 ) } ) ⊆ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
128 4 127 eqsstrid ⊢ ( 𝑅 ∈ TosetRel → 𝐶 ⊆ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
129 94 128 unssd ⊢ ( 𝑅 ∈ TosetRel → ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) ⊆ ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) )
130 92 129 eqssd ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝐴 ∪ 𝐵 ) ∪ 𝐶 ) )