Metamath Proof Explorer

Theorem tfsconcatlem

Description: Lemma for tfsconcatun . (Contributed by RP, 23-Feb-2025)

Ref Expression
Assertion tfsconcatlem 
|- ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> E! x E. y e. B ( C = ( A +o y ) /\ x = ( F ` y ) ) )

Proof

Step Hyp Ref Expression
1 onss 
 |-  ( B e. On -> B C_ On )
2 1 3ad2ant2 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> B C_ On )
3 oacl 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
4 eloni 
 |-  ( ( A +o B ) e. On -> Ord ( A +o B ) )
5 3 4 syl 
 |-  ( ( A e. On /\ B e. On ) -> Ord ( A +o B ) )
6 eloni 
 |-  ( A e. On -> Ord A )
7 6 adantr 
 |-  ( ( A e. On /\ B e. On ) -> Ord A )
8 ordeldif 
 |-  ( ( Ord ( A +o B ) /\ Ord A ) -> ( C e. ( ( A +o B ) \ A ) <-> ( C e. ( A +o B ) /\ A C_ C ) ) )
9 5 7 8 syl2anc 
 |-  ( ( A e. On /\ B e. On ) -> ( C e. ( ( A +o B ) \ A ) <-> ( C e. ( A +o B ) /\ A C_ C ) ) )
10 9 biimpa 
 |-  ( ( ( A e. On /\ B e. On ) /\ C e. ( ( A +o B ) \ A ) ) -> ( C e. ( A +o B ) /\ A C_ C ) )
11 10 ancomd 
 |-  ( ( ( A e. On /\ B e. On ) /\ C e. ( ( A +o B ) \ A ) ) -> ( A C_ C /\ C e. ( A +o B ) ) )
12 11 ex 
 |-  ( ( A e. On /\ B e. On ) -> ( C e. ( ( A +o B ) \ A ) -> ( A C_ C /\ C e. ( A +o B ) ) ) )
13 12 imdistani 
 |-  ( ( ( A e. On /\ B e. On ) /\ C e. ( ( A +o B ) \ A ) ) -> ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) )
14 13 3impa 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) )
15 oawordex2 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( A C_ C /\ C e. ( A +o B ) ) ) -> E. y e. B ( A +o y ) = C )
16 14 15 syl 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> E. y e. B ( A +o y ) = C )
17 simp1 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> A e. On )
18 onss 
 |-  ( ( A +o B ) e. On -> ( A +o B ) C_ On )
19 3 18 syl 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) C_ On )
20 19 ssdifd 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) \ A ) C_ ( On \ A ) )
21 20 sselda 
 |-  ( ( ( A e. On /\ B e. On ) /\ C e. ( ( A +o B ) \ A ) ) -> C e. ( On \ A ) )
22 21 3impa 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> C e. ( On \ A ) )
23 ordon 
 |-  Ord On
24 17 6 syl 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> Ord A )
25 ordeldif 
 |-  ( ( Ord On /\ Ord A ) -> ( C e. ( On \ A ) <-> ( C e. On /\ A C_ C ) ) )
26 23 24 25 sylancr 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> ( C e. ( On \ A ) <-> ( C e. On /\ A C_ C ) ) )
27 22 26 mpbid 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> ( C e. On /\ A C_ C ) )
28 anass 
 |-  ( ( ( A e. On /\ C e. On ) /\ A C_ C ) <-> ( A e. On /\ ( C e. On /\ A C_ C ) ) )
29 17 27 28 sylanbrc 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> ( ( A e. On /\ C e. On ) /\ A C_ C ) )
30 oawordeu 
 |-  ( ( ( A e. On /\ C e. On ) /\ A C_ C ) -> E! y e. On ( A +o y ) = C )
31 29 30 syl 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> E! y e. On ( A +o y ) = C )
32 reuss 
 |-  ( ( B C_ On /\ E. y e. B ( A +o y ) = C /\ E! y e. On ( A +o y ) = C ) -> E! y e. B ( A +o y ) = C )
33 2 16 31 32 syl3anc 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> E! y e. B ( A +o y ) = C )
34 reurmo 
 |-  ( E! y e. B ( A +o y ) = C -> E* y e. B ( A +o y ) = C )
35 33 34 syl 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> E* y e. B ( A +o y ) = C )
36 df-rmo 
 |-  ( E* y e. B ( A +o y ) = C <-> E* y ( y e. B /\ ( A +o y ) = C ) )
37 35 36 sylib 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> E* y ( y e. B /\ ( A +o y ) = C ) )
38 moeq 
 |-  E* x x = ( F ` y )
39 38 ax-gen 
 |-  A. y E* x x = ( F ` y )
40 moexexvw 
 |-  ( ( E* y ( y e. B /\ ( A +o y ) = C ) /\ A. y E* x x = ( F ` y ) ) -> E* x E. y ( ( y e. B /\ ( A +o y ) = C ) /\ x = ( F ` y ) ) )
41 37 39 40 sylancl 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> E* x E. y ( ( y e. B /\ ( A +o y ) = C ) /\ x = ( F ` y ) ) )
42 df-rex 
 |-  ( E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) <-> E. y ( y e. B /\ ( ( A +o y ) = C /\ x = ( F ` y ) ) ) )
43 anass 
 |-  ( ( ( y e. B /\ ( A +o y ) = C ) /\ x = ( F ` y ) ) <-> ( y e. B /\ ( ( A +o y ) = C /\ x = ( F ` y ) ) ) )
44 43 exbii 
 |-  ( E. y ( ( y e. B /\ ( A +o y ) = C ) /\ x = ( F ` y ) ) <-> E. y ( y e. B /\ ( ( A +o y ) = C /\ x = ( F ` y ) ) ) )
45 42 44 bitr4i 
 |-  ( E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) <-> E. y ( ( y e. B /\ ( A +o y ) = C ) /\ x = ( F ` y ) ) )
46 45 mobii 
 |-  ( E* x E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) <-> E* x E. y ( ( y e. B /\ ( A +o y ) = C ) /\ x = ( F ` y ) ) )
47 41 46 sylibr 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> E* x E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) )
48 fvex 
 |-  ( F ` y ) e. _V
49 48 isseti 
 |-  E. x x = ( F ` y )
50 49 jctr 
 |-  ( ( A +o y ) = C -> ( ( A +o y ) = C /\ E. x x = ( F ` y ) ) )
51 50 a1i 
 |-  ( ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) /\ y e. B ) -> ( ( A +o y ) = C -> ( ( A +o y ) = C /\ E. x x = ( F ` y ) ) ) )
52 51 reximdva 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> ( E. y e. B ( A +o y ) = C -> E. y e. B ( ( A +o y ) = C /\ E. x x = ( F ` y ) ) ) )
53 16 52 mpd 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> E. y e. B ( ( A +o y ) = C /\ E. x x = ( F ` y ) ) )
54 rexcom4a 
 |-  ( E. x E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) <-> E. y e. B ( ( A +o y ) = C /\ E. x x = ( F ` y ) ) )
55 exmoeu 
 |-  ( E. x E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) <-> ( E* x E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) -> E! x E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) ) )
56 54 55 bitr3i 
 |-  ( E. y e. B ( ( A +o y ) = C /\ E. x x = ( F ` y ) ) <-> ( E* x E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) -> E! x E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) ) )
57 53 56 sylib 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> ( E* x E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) -> E! x E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) ) )
58 47 57 mpd 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> E! x E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) )
59 eqcom 
 |-  ( ( A +o y ) = C <-> C = ( A +o y ) )
60 59 anbi1i 
 |-  ( ( ( A +o y ) = C /\ x = ( F ` y ) ) <-> ( C = ( A +o y ) /\ x = ( F ` y ) ) )
61 60 rexbii 
 |-  ( E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) <-> E. y e. B ( C = ( A +o y ) /\ x = ( F ` y ) ) )
62 61 eubii 
 |-  ( E! x E. y e. B ( ( A +o y ) = C /\ x = ( F ` y ) ) <-> E! x E. y e. B ( C = ( A +o y ) /\ x = ( F ` y ) ) )
63 58 62 sylib 
 |-  ( ( A e. On /\ B e. On /\ C e. ( ( A +o B ) \ A ) ) -> E! x E. y e. B ( C = ( A +o y ) /\ x = ( F ` y ) ) )