Metamath Proof Explorer

Theorem brtrclfv2

Description: Two ways to indicate two elements are related by the transitive closure of a relation. (Contributed by RP, 1-Jul-2020)

Ref Expression
Assertion brtrclfv2 ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ↔ 𝑌 ∈ ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } ) )

Proof

Step Hyp Ref Expression
1 df-br ⊢ ( 𝑋 ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
2 1 a1i ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑋 ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ) )
3 trclfv ⊢ ( 𝑅 ∈ 𝑊 → ( t+ ‘ 𝑅 ) = ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
4 3 breqd ⊢ ( 𝑅 ∈ 𝑊 → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ↔ 𝑋 ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑌 ) )
5 4 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ↔ 𝑋 ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑌 ) )
6 elimasng ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑌 ∈ ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } “ { 𝑋 } ) ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ) )
7 6 3adant3 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑌 ∈ ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } “ { 𝑋 } ) ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ) )
8 2 5 7 3bitr4d ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ↔ 𝑌 ∈ ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } “ { 𝑋 } ) ) )
9 intimasn ⊢ ( 𝑋 ∈ 𝑈 → ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } “ { 𝑋 } ) = ∩ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } )
10 9 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } “ { 𝑋 } ) = ∩ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } )
11 simpl3 ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → 𝑅 ∈ 𝑊 )
12 snex ⊢ { 𝑋 } ∈ V
13 vex ⊢ 𝑓 ∈ V
14 12 13 xpex ⊢ ( { 𝑋 } × 𝑓 ) ∈ V
15 unexg ⊢ ( ( 𝑅 ∈ 𝑊 ∧ ( { 𝑋 } × 𝑓 ) ∈ V ) → ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ∈ V )
16 11 14 15 sylancl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ∈ V )
17 trclfvlb ⊢ ( ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ∈ V → ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) )
18 17 unssad ⊢ ( ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ∈ V → 𝑅 ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) )
19 16 18 syl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → 𝑅 ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) )
20 trclfvcotrg ⊢ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∘ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ) ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) )
21 20 a1i ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∘ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ) ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) )
22 simpl1 ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → 𝑋 ∈ 𝑈 )
23 snidg ⊢ ( 𝑋 ∈ 𝑈 → 𝑋 ∈ { 𝑋 } )
24 22 23 syl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → 𝑋 ∈ { 𝑋 } )
25 inelcm ⊢ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑋 ∈ { 𝑋 } ) → ( { 𝑋 } ∩ { 𝑋 } ) ≠ ∅ )
26 24 24 25 syl2anc ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( { 𝑋 } ∩ { 𝑋 } ) ≠ ∅ )
27 xpima2 ⊢ ( ( { 𝑋 } ∩ { 𝑋 } ) ≠ ∅ → ( ( { 𝑋 } × 𝑓 ) “ { 𝑋 } ) = 𝑓 )
28 26 27 syl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( ( { 𝑋 } × 𝑓 ) “ { 𝑋 } ) = 𝑓 )
29 16 17 syl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) )
30 29 unssbd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( { 𝑋 } × 𝑓 ) ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) )
31 imass1 ⊢ ( ( { 𝑋 } × 𝑓 ) ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) → ( ( { 𝑋 } × 𝑓 ) “ { 𝑋 } ) ⊆ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ { 𝑋 } ) )
32 30 31 syl ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( ( { 𝑋 } × 𝑓 ) “ { 𝑋 } ) ⊆ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ { 𝑋 } ) )
33 28 32 eqsstrrd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → 𝑓 ⊆ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ { 𝑋 } ) )
34 imaundir ⊢ ( ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) “ ( { 𝑋 } ∪ 𝑓 ) ) = ( ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ∪ ( ( { 𝑋 } × 𝑓 ) “ ( { 𝑋 } ∪ 𝑓 ) ) )
35 simpr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 )
36 imassrn ⊢ ( ( { 𝑋 } × 𝑓 ) “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ ran ( { 𝑋 } × 𝑓 )
37 rnxpss ⊢ ran ( { 𝑋 } × 𝑓 ) ⊆ 𝑓
38 36 37 sstri ⊢ ( ( { 𝑋 } × 𝑓 ) “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓
39 38 a1i ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( ( { 𝑋 } × 𝑓 ) “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 )
40 35 39 unssd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ∪ ( ( { 𝑋 } × 𝑓 ) “ ( { 𝑋 } ∪ 𝑓 ) ) ) ⊆ 𝑓 )
41 34 40 eqsstrid ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 )
42 trclimalb2 ⊢ ( ( ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ∈ V ∧ ( ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ { 𝑋 } ) ⊆ 𝑓 )
43 16 41 42 syl2anc ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ { 𝑋 } ) ⊆ 𝑓 )
44 33 43 eqssd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → 𝑓 = ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ { 𝑋 } ) )
45 sbcan ⊢ ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑓 = ( 𝑟 “ { 𝑋 } ) ) ↔ ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] 𝑓 = ( 𝑟 “ { 𝑋 } ) ) )
46 sbcan ⊢ ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ↔ ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] 𝑅 ⊆ 𝑟 ∧ [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) )
47 fvex ⊢ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∈ V
48 sbcssg ⊢ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∈ V → ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] 𝑅 ⊆ 𝑟 ↔ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑅 ⊆ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 ) )
49 47 48 ax-mp ⊢ ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] 𝑅 ⊆ 𝑟 ↔ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑅 ⊆ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 )
50 csbconstg ⊢ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∈ V → ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑅 = 𝑅 )
51 47 50 ax-mp ⊢ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑅 = 𝑅
52 47 csbvargi ⊢ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 = ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) )
53 51 52 sseq12i ⊢ ( ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑅 ⊆ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 ↔ 𝑅 ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) )
54 49 53 bitri ⊢ ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] 𝑅 ⊆ 𝑟 ↔ 𝑅 ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) )
55 sbcssg ⊢ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∈ V → ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ↔ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ ( 𝑟 ∘ 𝑟 ) ⊆ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 ) )
56 47 55 ax-mp ⊢ ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ↔ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ ( 𝑟 ∘ 𝑟 ) ⊆ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 )
57 csbcog ⊢ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∈ V → ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ ( 𝑟 ∘ 𝑟 ) = ( ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 ∘ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 ) )
58 47 57 ax-mp ⊢ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ ( 𝑟 ∘ 𝑟 ) = ( ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 ∘ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 )
59 52 52 coeq12i ⊢ ( ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 ∘ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 ) = ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∘ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) )
60 58 59 eqtri ⊢ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ ( 𝑟 ∘ 𝑟 ) = ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∘ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) )
61 60 52 sseq12i ⊢ ( ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ ( 𝑟 ∘ 𝑟 ) ⊆ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 ↔ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∘ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ) ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) )
62 56 61 bitri ⊢ ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ↔ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∘ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ) ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) )
63 54 62 anbi12i ⊢ ( ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] 𝑅 ⊆ 𝑟 ∧ [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ↔ ( 𝑅 ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∧ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∘ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ) ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ) )
64 46 63 bitri ⊢ ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ↔ ( 𝑅 ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∧ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∘ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ) ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ) )
65 sbceq2g ⊢ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∈ V → ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] 𝑓 = ( 𝑟 “ { 𝑋 } ) ↔ 𝑓 = ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ ( 𝑟 “ { 𝑋 } ) ) )
66 47 65 ax-mp ⊢ ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] 𝑓 = ( 𝑟 “ { 𝑋 } ) ↔ 𝑓 = ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ ( 𝑟 “ { 𝑋 } ) )
67 csbima12 ⊢ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ ( 𝑟 “ { 𝑋 } ) = ( ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 “ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ { 𝑋 } )
68 52 imaeq1i ⊢ ( ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ 𝑟 “ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ { 𝑋 } ) = ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ { 𝑋 } )
69 csbconstg ⊢ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∈ V → ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ { 𝑋 } = { 𝑋 } )
70 47 69 ax-mp ⊢ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ { 𝑋 } = { 𝑋 }
71 70 imaeq2i ⊢ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ { 𝑋 } ) = ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ { 𝑋 } )
72 67 68 71 3eqtri ⊢ ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ ( 𝑟 “ { 𝑋 } ) = ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ { 𝑋 } )
73 72 eqeq2i ⊢ ( 𝑓 = ⦋ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ⦌ ( 𝑟 “ { 𝑋 } ) ↔ 𝑓 = ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ { 𝑋 } ) )
74 66 73 bitri ⊢ ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] 𝑓 = ( 𝑟 “ { 𝑋 } ) ↔ 𝑓 = ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ { 𝑋 } ) )
75 64 74 anbi12i ⊢ ( ( [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] 𝑓 = ( 𝑟 “ { 𝑋 } ) ) ↔ ( ( 𝑅 ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∧ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∘ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ) ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ) ∧ 𝑓 = ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ { 𝑋 } ) ) )
76 45 75 sylbbr ⊢ ( ( ( 𝑅 ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∧ ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ∘ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ) ⊆ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) ) ∧ 𝑓 = ( ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) “ { 𝑋 } ) ) → [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑓 = ( 𝑟 “ { 𝑋 } ) ) )
77 19 21 44 76 syl21anc ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → [ ( t+ ‘ ( 𝑅 ∪ ( { 𝑋 } × 𝑓 ) ) ) / 𝑟 ] ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑓 = ( 𝑟 “ { 𝑋 } ) ) )
78 77 spesbcd ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) ∧ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ) → ∃ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑓 = ( 𝑟 “ { 𝑋 } ) ) )
79 78 ex ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 → ∃ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑓 = ( 𝑟 “ { 𝑋 } ) ) ) )
80 eqeq1 ⊢ ( 𝑔 = 𝑓 → ( 𝑔 = ( 𝑠 “ { 𝑋 } ) ↔ 𝑓 = ( 𝑠 “ { 𝑋 } ) ) )
81 80 rexbidv ⊢ ( 𝑔 = 𝑓 → ( ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) ↔ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑓 = ( 𝑠 “ { 𝑋 } ) ) )
82 imaeq1 ⊢ ( 𝑠 = 𝑟 → ( 𝑠 “ { 𝑋 } ) = ( 𝑟 “ { 𝑋 } ) )
83 82 eqeq2d ⊢ ( 𝑠 = 𝑟 → ( 𝑓 = ( 𝑠 “ { 𝑋 } ) ↔ 𝑓 = ( 𝑟 “ { 𝑋 } ) ) )
84 83 rexab2 ⊢ ( ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑓 = ( 𝑠 “ { 𝑋 } ) ↔ ∃ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑓 = ( 𝑟 “ { 𝑋 } ) ) )
85 81 84 bitrdi ⊢ ( 𝑔 = 𝑓 → ( ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) ↔ ∃ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑓 = ( 𝑟 “ { 𝑋 } ) ) ) )
86 13 85 elab ⊢ ( 𝑓 ∈ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } ↔ ∃ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑓 = ( 𝑟 “ { 𝑋 } ) ) )
87 79 86 imbitrrdi ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 → 𝑓 ∈ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } ) )
88 intss1 ⊢ ( 𝑓 ∈ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } → ∩ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } ⊆ 𝑓 )
89 87 88 syl6 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 → ∩ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } ⊆ 𝑓 ) )
90 89 alrimiv ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ∀ 𝑓 ( ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 → ∩ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } ⊆ 𝑓 ) )
91 ssintab ⊢ ( ∩ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } ⊆ ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } ↔ ∀ 𝑓 ( ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 → ∩ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } ⊆ 𝑓 ) )
92 90 91 sylibr ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ∩ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } ⊆ ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } )
93 ssintab ⊢ ( ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } ⊆ ∩ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } ↔ ∀ 𝑔 ( ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) → ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } ⊆ 𝑔 ) )
94 82 eqeq2d ⊢ ( 𝑠 = 𝑟 → ( 𝑔 = ( 𝑠 “ { 𝑋 } ) ↔ 𝑔 = ( 𝑟 “ { 𝑋 } ) ) )
95 94 rexab2 ⊢ ( ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) ↔ ∃ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑔 = ( 𝑟 “ { 𝑋 } ) ) )
96 simpr ⊢ ( ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑔 = ( 𝑟 “ { 𝑋 } ) ) → 𝑔 = ( 𝑟 “ { 𝑋 } ) )
97 imass1 ⊢ ( 𝑅 ⊆ 𝑟 → ( 𝑅 “ { 𝑋 } ) ⊆ ( 𝑟 “ { 𝑋 } ) )
98 97 adantr ⊢ ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑅 “ { 𝑋 } ) ⊆ ( 𝑟 “ { 𝑋 } ) )
99 imass1 ⊢ ( 𝑅 ⊆ 𝑟 → ( 𝑅 “ ( 𝑟 “ { 𝑋 } ) ) ⊆ ( 𝑟 “ ( 𝑟 “ { 𝑋 } ) ) )
100 imaco ⊢ ( ( 𝑟 ∘ 𝑟 ) “ { 𝑋 } ) = ( 𝑟 “ ( 𝑟 “ { 𝑋 } ) )
101 imass1 ⊢ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 → ( ( 𝑟 ∘ 𝑟 ) “ { 𝑋 } ) ⊆ ( 𝑟 “ { 𝑋 } ) )
102 100 101 eqsstrrid ⊢ ( ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 → ( 𝑟 “ ( 𝑟 “ { 𝑋 } ) ) ⊆ ( 𝑟 “ { 𝑋 } ) )
103 99 102 sylan9ss ⊢ ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( 𝑅 “ ( 𝑟 “ { 𝑋 } ) ) ⊆ ( 𝑟 “ { 𝑋 } ) )
104 98 103 jca ⊢ ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) → ( ( 𝑅 “ { 𝑋 } ) ⊆ ( 𝑟 “ { 𝑋 } ) ∧ ( 𝑅 “ ( 𝑟 “ { 𝑋 } ) ) ⊆ ( 𝑟 “ { 𝑋 } ) ) )
105 104 adantr ⊢ ( ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑔 = ( 𝑟 “ { 𝑋 } ) ) → ( ( 𝑅 “ { 𝑋 } ) ⊆ ( 𝑟 “ { 𝑋 } ) ∧ ( 𝑅 “ ( 𝑟 “ { 𝑋 } ) ) ⊆ ( 𝑟 “ { 𝑋 } ) ) )
106 vex ⊢ 𝑟 ∈ V
107 106 imaex ⊢ ( 𝑟 “ { 𝑋 } ) ∈ V
108 imaundi ⊢ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) = ( ( 𝑅 “ { 𝑋 } ) ∪ ( 𝑅 “ 𝑓 ) )
109 108 sseq1i ⊢ ( ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ↔ ( ( 𝑅 “ { 𝑋 } ) ∪ ( 𝑅 “ 𝑓 ) ) ⊆ 𝑓 )
110 unss ⊢ ( ( ( 𝑅 “ { 𝑋 } ) ⊆ 𝑓 ∧ ( 𝑅 “ 𝑓 ) ⊆ 𝑓 ) ↔ ( ( 𝑅 “ { 𝑋 } ) ∪ ( 𝑅 “ 𝑓 ) ) ⊆ 𝑓 )
111 109 110 bitr4i ⊢ ( ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ↔ ( ( 𝑅 “ { 𝑋 } ) ⊆ 𝑓 ∧ ( 𝑅 “ 𝑓 ) ⊆ 𝑓 ) )
112 imaeq2 ⊢ ( 𝑓 = ( 𝑟 “ { 𝑋 } ) → ( 𝑅 “ 𝑓 ) = ( 𝑅 “ ( 𝑟 “ { 𝑋 } ) ) )
113 id ⊢ ( 𝑓 = ( 𝑟 “ { 𝑋 } ) → 𝑓 = ( 𝑟 “ { 𝑋 } ) )
114 112 113 sseq12d ⊢ ( 𝑓 = ( 𝑟 “ { 𝑋 } ) → ( ( 𝑅 “ 𝑓 ) ⊆ 𝑓 ↔ ( 𝑅 “ ( 𝑟 “ { 𝑋 } ) ) ⊆ ( 𝑟 “ { 𝑋 } ) ) )
115 114 cleq2lem ⊢ ( 𝑓 = ( 𝑟 “ { 𝑋 } ) → ( ( ( 𝑅 “ { 𝑋 } ) ⊆ 𝑓 ∧ ( 𝑅 “ 𝑓 ) ⊆ 𝑓 ) ↔ ( ( 𝑅 “ { 𝑋 } ) ⊆ ( 𝑟 “ { 𝑋 } ) ∧ ( 𝑅 “ ( 𝑟 “ { 𝑋 } ) ) ⊆ ( 𝑟 “ { 𝑋 } ) ) ) )
116 111 115 bitrid ⊢ ( 𝑓 = ( 𝑟 “ { 𝑋 } ) → ( ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 ↔ ( ( 𝑅 “ { 𝑋 } ) ⊆ ( 𝑟 “ { 𝑋 } ) ∧ ( 𝑅 “ ( 𝑟 “ { 𝑋 } ) ) ⊆ ( 𝑟 “ { 𝑋 } ) ) ) )
117 107 116 elab ⊢ ( ( 𝑟 “ { 𝑋 } ) ∈ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } ↔ ( ( 𝑅 “ { 𝑋 } ) ⊆ ( 𝑟 “ { 𝑋 } ) ∧ ( 𝑅 “ ( 𝑟 “ { 𝑋 } ) ) ⊆ ( 𝑟 “ { 𝑋 } ) ) )
118 105 117 sylibr ⊢ ( ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑔 = ( 𝑟 “ { 𝑋 } ) ) → ( 𝑟 “ { 𝑋 } ) ∈ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } )
119 96 118 eqeltrd ⊢ ( ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑔 = ( 𝑟 “ { 𝑋 } ) ) → 𝑔 ∈ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } )
120 119 exlimiv ⊢ ( ∃ 𝑟 ( ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) ∧ 𝑔 = ( 𝑟 “ { 𝑋 } ) ) → 𝑔 ∈ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } )
121 95 120 sylbi ⊢ ( ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) → 𝑔 ∈ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } )
122 intss1 ⊢ ( 𝑔 ∈ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } → ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } ⊆ 𝑔 )
123 121 122 syl ⊢ ( ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) → ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } ⊆ 𝑔 )
124 93 123 mpgbir ⊢ ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } ⊆ ∩ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) }
125 124 a1i ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } ⊆ ∩ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } )
126 92 125 eqssd ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ∩ { 𝑔 ∣ ∃ 𝑠 ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } 𝑔 = ( 𝑠 “ { 𝑋 } ) } = ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } )
127 10 126 eqtrd ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } “ { 𝑋 } ) = ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } )
128 127 eleq2d ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑌 ∈ ( ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } “ { 𝑋 } ) ↔ 𝑌 ∈ ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } ) )
129 8 128 bitrd ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑋 ( t+ ‘ 𝑅 ) 𝑌 ↔ 𝑌 ∈ ∩ { 𝑓 ∣ ( 𝑅 “ ( { 𝑋 } ∪ 𝑓 ) ) ⊆ 𝑓 } ) )