Metamath Proof Explorer

Theorem phpreu

Description: Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Assertion phpreu ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
2 1 biimpac ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶 ) → 𝐶 ∈ 𝐴 )
3 rabid ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↔ ( 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ) )
4 3 simplbi2com ⊢ ( 𝐶 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ) )
5 2 4 syl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = 𝐶 ) → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ) )
6 5 impancom ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝐶 → 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ) )
7 6 ancrd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝐶 → ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 ) ) )
8 7 expimpd ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 = 𝐶 ) → ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 ) ) )
9 8 reximdv2 ⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑥 = 𝐶 ) )
10 9 ralimia ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑥 = 𝐶 )
11 3 simplbi ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } → 𝑦 ∈ 𝐵 )
12 6 pm4.71rd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝐶 ↔ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 ) ) )
13 df-mpt ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) = { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 ) }
14 13 breqi ⊢ ( 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ↔ 𝑦 { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 ) } 𝑥 )
15 df-br ⊢ ( 𝑦 { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 ) } 𝑥 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 ) } )
16 opabidw ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 ) } ↔ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 ) )
17 14 15 16 3bitri ⊢ ( 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ↔ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 ) )
18 12 17 bitr4di ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 = 𝐶 ↔ 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ) )
19 11 18 sylan2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ) → ( 𝑥 = 𝐶 ↔ 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ) )
20 19 rexbidva ⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑥 = 𝐶 ↔ ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ) )
21 20 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑥 = 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 )
22 breq2 ⊢ ( 𝑎 = 𝑥 → ( 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 ↔ 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ) )
23 22 rexbidv ⊢ ( 𝑎 = 𝑥 → ( ∃ 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 ↔ ∃ 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ) )
24 nfcv ⊢ Ⅎ 𝑏 { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 }
25 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 }
26 nfcv ⊢ Ⅎ 𝑦 𝑏
27 nfmpt1 ⊢ Ⅎ 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 )
28 nfcv ⊢ Ⅎ 𝑦 𝑥
29 26 27 28 nfbr ⊢ Ⅎ 𝑦 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥
30 nfv ⊢ Ⅎ 𝑏 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥
31 breq1 ⊢ ( 𝑏 = 𝑦 → ( 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ↔ 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ) )
32 24 25 29 30 31 cbvrexfw ⊢ ( ∃ 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ↔ ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 )
33 23 32 bitrdi ⊢ ( 𝑎 = 𝑥 → ( ∃ 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 ↔ ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ) )
34 33 cbvralvw ⊢ ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 )
35 21 34 bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑥 = 𝐶 ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 )
36 10 35 sylib ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 )
37 nfv ⊢ Ⅎ 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 )
38 25 nfcri ⊢ Ⅎ 𝑦 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 }
39 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑏 / 𝑦 ⦌ 𝐶
40 39 nfeq2 ⊢ Ⅎ 𝑦 𝑥 = ⦋ 𝑏 / 𝑦 ⦌ 𝐶
41 38 40 nfan ⊢ Ⅎ 𝑦 ( 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = ⦋ 𝑏 / 𝑦 ⦌ 𝐶 )
42 eleq1 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↔ 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ) )
43 csbeq1a ⊢ ( 𝑦 = 𝑏 → 𝐶 = ⦋ 𝑏 / 𝑦 ⦌ 𝐶 )
44 43 eqeq2d ⊢ ( 𝑦 = 𝑏 → ( 𝑥 = 𝐶 ↔ 𝑥 = ⦋ 𝑏 / 𝑦 ⦌ 𝐶 ) )
45 42 44 anbi12d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 ) ↔ ( 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = ⦋ 𝑏 / 𝑦 ⦌ 𝐶 ) ) )
46 37 41 45 cbvopab1 ⊢ { ⟨ 𝑦 , 𝑥 ⟩ ∣ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = 𝐶 ) } = { ⟨ 𝑏 , 𝑥 ⟩ ∣ ( 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = ⦋ 𝑏 / 𝑦 ⦌ 𝐶 ) }
47 df-mpt ⊢ ( 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 ) = { ⟨ 𝑏 , 𝑥 ⟩ ∣ ( 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∧ 𝑥 = ⦋ 𝑏 / 𝑦 ⦌ 𝐶 ) }
48 46 13 47 3eqtr4i ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) = ( 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 )
49 nfcv ⊢ Ⅎ 𝑦 𝐵
50 39 nfel1 ⊢ Ⅎ 𝑦 ⦋ 𝑏 / 𝑦 ⦌ 𝐶 ∈ 𝐴
51 43 eleq1d ⊢ ( 𝑦 = 𝑏 → ( 𝐶 ∈ 𝐴 ↔ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 ∈ 𝐴 ) )
52 26 49 50 51 elrabf ⊢ ( 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↔ ( 𝑏 ∈ 𝐵 ∧ ⦋ 𝑏 / 𝑦 ⦌ 𝐶 ∈ 𝐴 ) )
53 52 simprbi ⊢ ( 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } → ⦋ 𝑏 / 𝑦 ⦌ 𝐶 ∈ 𝐴 )
54 48 53 fmpti ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ⟶ 𝐴
55 36 54 jctil ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 → ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ⟶ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 ) )
56 dffo4 ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –onto→ 𝐴 ↔ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ⟶ 𝐴 ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 ) )
57 55 56 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 → ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –onto→ 𝐴 )
58 57 adantl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) → ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –onto→ 𝐴 )
59 relen ⊢ Rel ≈
60 59 brrelex2i ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ∈ V )
61 ssrab2 ⊢ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ⊆ 𝐵
62 ssdomg ⊢ ( 𝐵 ∈ V → ( { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ⊆ 𝐵 → { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ≼ 𝐵 ) )
63 60 61 62 mpisyl ⊢ ( 𝐴 ≈ 𝐵 → { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ≼ 𝐵 )
64 ensym ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴 )
65 domentr ⊢ ( ( { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ≼ 𝐵 ∧ 𝐵 ≈ 𝐴 ) → { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ≼ 𝐴 )
66 63 64 65 syl2anc ⊢ ( 𝐴 ≈ 𝐵 → { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ≼ 𝐴 )
67 66 ad2antlr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) → { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ≼ 𝐴 )
68 enfi ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ Fin ↔ 𝐵 ∈ Fin ) )
69 68 biimpac ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐵 ∈ Fin )
70 rabfi ⊢ ( 𝐵 ∈ Fin → { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∈ Fin )
71 69 70 syl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∈ Fin )
72 fodomfi ⊢ ( ( { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ∈ Fin ∧ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –onto→ 𝐴 ) → 𝐴 ≼ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } )
73 71 57 72 syl2an ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) → 𝐴 ≼ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } )
74 sbth ⊢ ( ( { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ≼ 𝐴 ∧ 𝐴 ≼ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ) → { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ≈ 𝐴 )
75 67 73 74 syl2anc ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) → { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ≈ 𝐴 )
76 simpll ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) → 𝐴 ∈ Fin )
77 fofinf1o ⊢ ( ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –onto→ 𝐴 ∧ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ≈ 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –1-1-onto→ 𝐴 )
78 58 75 76 77 syl3anc ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) → ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –1-1-onto→ 𝐴 )
79 f1of1 ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –1-1-onto→ 𝐴 → ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –1-1→ 𝐴 )
80 78 79 syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) → ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –1-1→ 𝐴 )
81 dff12 ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –1-1→ 𝐴 ↔ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ⟶ 𝐴 ∧ ∀ 𝑎 ∃* 𝑏 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 ) )
82 81 simprbi ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –1-1→ 𝐴 → ∀ 𝑎 ∃* 𝑏 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 )
83 22 mobidv ⊢ ( 𝑎 = 𝑥 → ( ∃* 𝑏 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 ↔ ∃* 𝑏 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ) )
84 29 30 31 cbvmow ⊢ ( ∃* 𝑏 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ↔ ∃* 𝑦 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 )
85 83 84 bitrdi ⊢ ( 𝑎 = 𝑥 → ( ∃* 𝑏 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 ↔ ∃* 𝑦 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ) )
86 85 cbvalvw ⊢ ( ∀ 𝑎 ∃* 𝑏 𝑏 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑎 ↔ ∀ 𝑥 ∃* 𝑦 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 )
87 82 86 sylib ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) : { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } –1-1→ 𝐴 → ∀ 𝑥 ∃* 𝑦 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 )
88 mormo ⊢ ( ∃* 𝑦 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 → ∃* 𝑦 ∈ 𝐵 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 )
89 88 alimi ⊢ ( ∀ 𝑥 ∃* 𝑦 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 → ∀ 𝑥 ∃* 𝑦 ∈ 𝐵 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 )
90 alral ⊢ ( ∀ 𝑥 ∃* 𝑦 ∈ 𝐵 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 → ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 )
91 80 87 89 90 4syl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 )
92 18 rmobidva ⊢ ( 𝑥 ∈ 𝐴 → ( ∃* 𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∃* 𝑦 ∈ 𝐵 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 ) )
93 92 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝑦 ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝐶 ∈ 𝐴 } ↦ 𝐶 ) 𝑥 )
94 91 93 sylibr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) → ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝑥 = 𝐶 )
95 94 ex ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 → ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) )
96 95 pm4.71d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) ) )
97 reu5 ⊢ ( ∃! 𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ( ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃* 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) )
98 97 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃* 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) )
99 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∃* 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) )
100 98 99 bitri ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) )
101 96 100 bitr4di ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝑥 = 𝐶 ) )