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 sselid ( ( 𝑅 ∈ 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 sselid ( ( 𝑅 ∈ 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 sselid ( ( 𝑅 ∈ 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 ‘ ( 𝐴𝐵 ) ) = ( ( 𝐴𝐵 ) ∪ 𝐶 ) )