Metamath Proof Explorer

Theorem ordtbaslem

Description: Lemma for ordtbas . In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses ordtval.1 ⊢ 𝑋 = dom 𝑅
ordtval.2 ⊢ 𝐴 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
Assertion ordtbaslem ( 𝑅 ∈ TosetRel → ( fi ‘ 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 ordtval.1 ⊢ 𝑋 = dom 𝑅
2 ordtval.2 ⊢ 𝐴 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
3 3anrot ⊢ ( ( 𝑦 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ↔ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) )
4 1 tsrlemax ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) ↔ ( 𝑦 𝑅 𝑎 ∨ 𝑦 𝑅 𝑏 ) ) )
5 3 4 sylan2br ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) ↔ ( 𝑦 𝑅 𝑎 ∨ 𝑦 𝑅 𝑏 ) ) )
6 5 3exp2 ⊢ ( 𝑅 ∈ TosetRel → ( 𝑎 ∈ 𝑋 → ( 𝑏 ∈ 𝑋 → ( 𝑦 ∈ 𝑋 → ( 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) ↔ ( 𝑦 𝑅 𝑎 ∨ 𝑦 𝑅 𝑏 ) ) ) ) ) )
7 6 imp42 ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) ↔ ( 𝑦 𝑅 𝑎 ∨ 𝑦 𝑅 𝑏 ) ) )
8 7 notbid ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ¬ 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) ↔ ¬ ( 𝑦 𝑅 𝑎 ∨ 𝑦 𝑅 𝑏 ) ) )
9 ioran ⊢ ( ¬ ( 𝑦 𝑅 𝑎 ∨ 𝑦 𝑅 𝑏 ) ↔ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) )
10 8 9 bitrdi ⊢ ( ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ 𝑦 ∈ 𝑋 ) → ( ¬ 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) ↔ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) ) )
11 10 rabbidva ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) } = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) } )
12 ifcl ⊢ ( ( 𝑏 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ) → if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) ∈ 𝑋 )
13 12 ancoms ⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) ∈ 𝑋 )
14 dmexg ⊢ ( 𝑅 ∈ TosetRel → dom 𝑅 ∈ V )
15 1 14 eqeltrid ⊢ ( 𝑅 ∈ TosetRel → 𝑋 ∈ V )
16 15 adantr ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → 𝑋 ∈ V )
17 rabexg ⊢ ( 𝑋 ∈ V → { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) } ∈ V )
18 16 17 syl ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) } ∈ V )
19 11 18 eqeltrd ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) } ∈ V )
20 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
21 breq2 ⊢ ( 𝑥 = if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) ) )
22 21 notbid ⊢ ( 𝑥 = if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) ) )
23 22 rabbidv ⊢ ( 𝑥 = if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) } )
24 20 23 elrnmpt1s ⊢ ( ( if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) ∈ 𝑋 ∧ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) } ∈ V ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) } ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
25 24 2 eleqtrrdi ⊢ ( ( if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) ∈ 𝑋 ∧ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) } ∈ V ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) } ∈ 𝐴 )
26 13 19 25 syl2an2 ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 if ( 𝑎 𝑅 𝑏 , 𝑏 , 𝑎 ) } ∈ 𝐴 )
27 11 26 eqeltrrd ⊢ ( ( 𝑅 ∈ TosetRel ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) } ∈ 𝐴 )
28 27 ralrimivva ⊢ ( 𝑅 ∈ TosetRel → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) } ∈ 𝐴 )
29 rabexg ⊢ ( 𝑋 ∈ V → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ V )
30 15 29 syl ⊢ ( 𝑅 ∈ TosetRel → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ V )
31 30 ralrimivw ⊢ ( 𝑅 ∈ TosetRel → ∀ 𝑎 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ V )
32 breq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝑎 ) )
33 32 notbid ⊢ ( 𝑥 = 𝑎 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝑎 ) )
34 33 rabbidv ⊢ ( 𝑥 = 𝑎 → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } )
35 34 cbvmptv ⊢ ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) = ( 𝑎 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } )
36 ineq1 ⊢ ( 𝑧 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } → ( 𝑧 ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) = ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) )
37 inrab ⊢ ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) }
38 36 37 eqtrdi ⊢ ( 𝑧 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } → ( 𝑧 ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) = { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) } )
39 38 eleq1d ⊢ ( 𝑧 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } → ( ( 𝑧 ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) ∈ 𝐴 ↔ { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) } ∈ 𝐴 ) )
40 39 ralbidv ⊢ ( 𝑧 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } → ( ∀ 𝑏 ∈ 𝑋 ( 𝑧 ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) ∈ 𝐴 ↔ ∀ 𝑏 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) } ∈ 𝐴 ) )
41 35 40 ralrnmptw ⊢ ( ∀ 𝑎 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑎 } ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∀ 𝑏 ∈ 𝑋 ( 𝑧 ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) ∈ 𝐴 ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) } ∈ 𝐴 ) )
42 31 41 syl ⊢ ( 𝑅 ∈ TosetRel → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∀ 𝑏 ∈ 𝑋 ( 𝑧 ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) ∈ 𝐴 ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ( ¬ 𝑦 𝑅 𝑎 ∧ ¬ 𝑦 𝑅 𝑏 ) } ∈ 𝐴 ) )
43 28 42 mpbird ⊢ ( 𝑅 ∈ TosetRel → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∀ 𝑏 ∈ 𝑋 ( 𝑧 ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) ∈ 𝐴 )
44 rabexg ⊢ ( 𝑋 ∈ V → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ∈ V )
45 15 44 syl ⊢ ( 𝑅 ∈ TosetRel → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ∈ V )
46 45 ralrimivw ⊢ ( 𝑅 ∈ TosetRel → ∀ 𝑏 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ∈ V )
47 breq2 ⊢ ( 𝑥 = 𝑏 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 𝑏 ) )
48 47 notbid ⊢ ( 𝑥 = 𝑏 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 𝑅 𝑏 ) )
49 48 rabbidv ⊢ ( 𝑥 = 𝑏 → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } )
50 49 cbvmptv ⊢ ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) = ( 𝑏 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } )
51 ineq2 ⊢ ( 𝑤 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } → ( 𝑧 ∩ 𝑤 ) = ( 𝑧 ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) )
52 51 eleq1d ⊢ ( 𝑤 = { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } → ( ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ↔ ( 𝑧 ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) ∈ 𝐴 ) )
53 50 52 ralrnmptw ⊢ ( ∀ 𝑏 ∈ 𝑋 { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ∈ V → ( ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ↔ ∀ 𝑏 ∈ 𝑋 ( 𝑧 ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) ∈ 𝐴 ) )
54 46 53 syl ⊢ ( 𝑅 ∈ TosetRel → ( ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ↔ ∀ 𝑏 ∈ 𝑋 ( 𝑧 ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) ∈ 𝐴 ) )
55 54 ralbidv ⊢ ( 𝑅 ∈ TosetRel → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∀ 𝑏 ∈ 𝑋 ( 𝑧 ∩ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑏 } ) ∈ 𝐴 ) )
56 43 55 mpbird ⊢ ( 𝑅 ∈ TosetRel → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 )
57 2 raleqi ⊢ ( ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ↔ ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 )
58 2 57 raleqbii ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 )
59 56 58 sylibr ⊢ ( 𝑅 ∈ TosetRel → ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 )
60 15 pwexd ⊢ ( 𝑅 ∈ TosetRel → 𝒫 𝑋 ∈ V )
61 ssrab2 ⊢ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ⊆ 𝑋
62 15 adantr ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ V )
63 elpw2g ⊢ ( 𝑋 ∈ V → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ∈ 𝒫 𝑋 ↔ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ⊆ 𝑋 ) )
64 62 63 syl ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋 ) → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ∈ 𝒫 𝑋 ↔ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ⊆ 𝑋 ) )
65 61 64 mpbiri ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑥 ∈ 𝑋 ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ∈ 𝒫 𝑋 )
66 65 fmpttd ⊢ ( 𝑅 ∈ TosetRel → ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) : 𝑋 ⟶ 𝒫 𝑋 )
67 66 frnd ⊢ ( 𝑅 ∈ TosetRel → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ⊆ 𝒫 𝑋 )
68 2 67 eqsstrid ⊢ ( 𝑅 ∈ TosetRel → 𝐴 ⊆ 𝒫 𝑋 )
69 60 68 ssexd ⊢ ( 𝑅 ∈ TosetRel → 𝐴 ∈ V )
70 inficl ⊢ ( 𝐴 ∈ V → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ↔ ( fi ‘ 𝐴 ) = 𝐴 ) )
71 69 70 syl ⊢ ( 𝑅 ∈ TosetRel → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 ∩ 𝑤 ) ∈ 𝐴 ↔ ( fi ‘ 𝐴 ) = 𝐴 ) )
72 59 71 mpbid ⊢ ( 𝑅 ∈ TosetRel → ( fi ‘ 𝐴 ) = 𝐴 )