Step | Hyp | Ref
| Expression |
1 | | iundomg.2 |
. . 3
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵) ∈ AC 𝐴) |
2 | | iundomg.3 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ≼ 𝐶) |
3 | | brdomi 7852 |
. . . . . . . . 9
⊢ (𝐵 ≼ 𝐶 → ∃𝑔 𝑔:𝐵–1-1→𝐶) |
4 | 3 | adantl 481 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → ∃𝑔 𝑔:𝐵–1-1→𝐶) |
5 | | f1f 6014 |
. . . . . . . . . . . 12
⊢ (𝑔:𝐵–1-1→𝐶 → 𝑔:𝐵⟶𝐶) |
6 | | reldom 7847 |
. . . . . . . . . . . . . . 15
⊢ Rel
≼ |
7 | 6 | brrelex2i 5083 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ≼ 𝐶 → 𝐶 ∈ V) |
8 | 6 | brrelexi 5082 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ≼ 𝐶 → 𝐵 ∈ V) |
9 | 7, 8 | elmapd 7758 |
. . . . . . . . . . . . 13
⊢ (𝐵 ≼ 𝐶 → (𝑔 ∈ (𝐶 ↑𝑚 𝐵) ↔ 𝑔:𝐵⟶𝐶)) |
10 | 9 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (𝑔 ∈ (𝐶 ↑𝑚 𝐵) ↔ 𝑔:𝐵⟶𝐶)) |
11 | 5, 10 | syl5ibr 235 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (𝑔:𝐵–1-1→𝐶 → 𝑔 ∈ (𝐶 ↑𝑚 𝐵))) |
12 | | ssiun2 4499 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 → (𝐶 ↑𝑚 𝐵) ⊆ ∪ 𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)) |
13 | 12 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (𝐶 ↑𝑚 𝐵) ⊆ ∪ 𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)) |
14 | 13 | sseld 3567 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (𝑔 ∈ (𝐶 ↑𝑚 𝐵) → 𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵))) |
15 | 11, 14 | syld 46 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (𝑔:𝐵–1-1→𝐶 → 𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵))) |
16 | 15 | ancrd 575 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (𝑔:𝐵–1-1→𝐶 → (𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵) ∧ 𝑔:𝐵–1-1→𝐶))) |
17 | 16 | eximdv 1833 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → (∃𝑔 𝑔:𝐵–1-1→𝐶 → ∃𝑔(𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵) ∧ 𝑔:𝐵–1-1→𝐶))) |
18 | 4, 17 | mpd 15 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → ∃𝑔(𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵) ∧ 𝑔:𝐵–1-1→𝐶)) |
19 | | df-rex 2902 |
. . . . . . 7
⊢
(∃𝑔 ∈
∪ 𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)𝑔:𝐵–1-1→𝐶 ↔ ∃𝑔(𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵) ∧ 𝑔:𝐵–1-1→𝐶)) |
20 | 18, 19 | sylibr 223 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ≼ 𝐶) → ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)𝑔:𝐵–1-1→𝐶) |
21 | 20 | ralimiaa 2935 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ≼ 𝐶 → ∀𝑥 ∈ 𝐴 ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)𝑔:𝐵–1-1→𝐶) |
22 | 2, 21 | syl 17 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)𝑔:𝐵–1-1→𝐶) |
23 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑦∃𝑔 ∈ ∪ 𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)𝑔:𝐵–1-1→𝐶 |
24 | | nfiu1 4486 |
. . . . . 6
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵) |
25 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥𝑔 |
26 | | nfcsb1v 3515 |
. . . . . . 7
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
27 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥𝐶 |
28 | 25, 26, 27 | nff1 6012 |
. . . . . 6
⊢
Ⅎ𝑥 𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶 |
29 | 24, 28 | nfrex 2990 |
. . . . 5
⊢
Ⅎ𝑥∃𝑔 ∈ ∪ 𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶 |
30 | | csbeq1a 3508 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
31 | | f1eq2 6010 |
. . . . . . 7
⊢ (𝐵 = ⦋𝑦 / 𝑥⦌𝐵 → (𝑔:𝐵–1-1→𝐶 ↔ 𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑔:𝐵–1-1→𝐶 ↔ 𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
33 | 32 | rexbidv 3034 |
. . . . 5
⊢ (𝑥 = 𝑦 → (∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)𝑔:𝐵–1-1→𝐶 ↔ ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
34 | 23, 29, 33 | cbvral 3143 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)𝑔:𝐵–1-1→𝐶 ↔ ∀𝑦 ∈ 𝐴 ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶) |
35 | 22, 34 | sylib 207 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶) |
36 | | f1eq1 6009 |
. . . 4
⊢ (𝑔 = (𝑓‘𝑦) → (𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶 ↔ (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
37 | 36 | acni3 8753 |
. . 3
⊢
((∪ 𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵) ∈ AC 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∃𝑔 ∈ ∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵)𝑔:⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶) → ∃𝑓(𝑓:𝐴⟶∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵) ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
38 | 1, 35, 37 | syl2anc 691 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:𝐴⟶∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵) ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
39 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑦(𝑓‘𝑥):𝐵–1-1→𝐶 |
40 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑓‘𝑦) |
41 | 40, 26, 27 | nff1 6012 |
. . . . . 6
⊢
Ⅎ𝑥(𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶 |
42 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑓‘𝑥) = (𝑓‘𝑦)) |
43 | | f1eq1 6009 |
. . . . . . . 8
⊢ ((𝑓‘𝑥) = (𝑓‘𝑦) → ((𝑓‘𝑥):𝐵–1-1→𝐶 ↔ (𝑓‘𝑦):𝐵–1-1→𝐶)) |
44 | 42, 43 | syl 17 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑓‘𝑥):𝐵–1-1→𝐶 ↔ (𝑓‘𝑦):𝐵–1-1→𝐶)) |
45 | | f1eq2 6010 |
. . . . . . . 8
⊢ (𝐵 = ⦋𝑦 / 𝑥⦌𝐵 → ((𝑓‘𝑦):𝐵–1-1→𝐶 ↔ (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
46 | 30, 45 | syl 17 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑓‘𝑦):𝐵–1-1→𝐶 ↔ (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
47 | 44, 46 | bitrd 267 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑓‘𝑥):𝐵–1-1→𝐶 ↔ (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶)) |
48 | 39, 41, 47 | cbvral 3143 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ↔ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶) |
49 | | df-ne 2782 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
50 | | acnrcl 8748 |
. . . . . . . . . 10
⊢ (∪ 𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵) ∈ AC 𝐴 → 𝐴 ∈ V) |
51 | 1, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ V) |
52 | | r19.2z 4012 |
. . . . . . . . . . . 12
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ≼ 𝐶) → ∃𝑥 ∈ 𝐴 𝐵 ≼ 𝐶) |
53 | 7 | rexlimivw 3011 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
𝐴 𝐵 ≼ 𝐶 → 𝐶 ∈ V) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝐵 ≼ 𝐶) → 𝐶 ∈ V) |
55 | 54 | expcom 450 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 𝐵 ≼ 𝐶 → (𝐴 ≠ ∅ → 𝐶 ∈ V)) |
56 | 2, 55 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ≠ ∅ → 𝐶 ∈ V)) |
57 | | xpexg 6858 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 × 𝐶) ∈ V) |
58 | 51, 56, 57 | syl6an 566 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ≠ ∅ → (𝐴 × 𝐶) ∈ V)) |
59 | 49, 58 | syl5bir 232 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝐴 = ∅ → (𝐴 × 𝐶) ∈ V)) |
60 | | xpeq1 5052 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (𝐴 × 𝐶) = (∅ × 𝐶)) |
61 | | 0xp 5122 |
. . . . . . . . 9
⊢ (∅
× 𝐶) =
∅ |
62 | | 0ex 4718 |
. . . . . . . . 9
⊢ ∅
∈ V |
63 | 61, 62 | eqeltri 2684 |
. . . . . . . 8
⊢ (∅
× 𝐶) ∈
V |
64 | 60, 63 | syl6eqel 2696 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝐴 × 𝐶) ∈ V) |
65 | 59, 64 | pm2.61d2 171 |
. . . . . 6
⊢ (𝜑 → (𝐴 × 𝐶) ∈ V) |
66 | | iunfo.1 |
. . . . . . . . . 10
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
67 | 66 | eleq2i 2680 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑇 ↔ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
68 | | eliun 4460 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵)) |
69 | 67, 68 | bitri 263 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑇 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵)) |
70 | | r19.29 3054 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → ∃𝑥 ∈ 𝐴 ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) |
71 | | xp1st 7089 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ({𝑥} × 𝐵) → (1st ‘𝑦) ∈ {𝑥}) |
72 | 71 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (1st ‘𝑦) ∈ {𝑥}) |
73 | | elsni 4142 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑦) ∈ {𝑥} → (1st ‘𝑦) = 𝑥) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (1st ‘𝑦) = 𝑥) |
75 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥 ∈ 𝐴) |
76 | 74, 75 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (1st ‘𝑦) ∈ 𝐴) |
77 | 74 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓‘(1st ‘𝑦)) = (𝑓‘𝑥)) |
78 | 77 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘𝑥)‘(2nd ‘𝑦))) |
79 | | f1f 6014 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓‘𝑥):𝐵–1-1→𝐶 → (𝑓‘𝑥):𝐵⟶𝐶) |
80 | 79 | ad2antrl 760 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓‘𝑥):𝐵⟶𝐶) |
81 | | xp2nd 7090 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑦) ∈ 𝐵) |
82 | 81 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (2nd ‘𝑦) ∈ 𝐵) |
83 | 80, 82 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘𝑥)‘(2nd ‘𝑦)) ∈ 𝐶) |
84 | 78, 83 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) ∈ 𝐶) |
85 | | opelxpi 5072 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑦) ∈ 𝐴 ∧ ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) ∈ 𝐶) → 〈(1st
‘𝑦), ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑦))〉 ∈ (𝐴 × 𝐶)) |
86 | 76, 84, 85 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → 〈(1st
‘𝑦), ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑦))〉 ∈ (𝐴 × 𝐶)) |
87 | 86 | rexlimiva 3010 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝐴 ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵)) → 〈(1st ‘𝑦), ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦))〉 ∈
(𝐴 × 𝐶)) |
88 | 70, 87 | syl 17 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → 〈(1st ‘𝑦), ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦))〉 ∈
(𝐴 × 𝐶)) |
89 | 88 | ex 449 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → (∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵) → 〈(1st ‘𝑦), ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦))〉 ∈
(𝐴 × 𝐶))) |
90 | 69, 89 | syl5bi 231 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → (𝑦 ∈ 𝑇 → 〈(1st ‘𝑦), ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦))〉 ∈
(𝐴 × 𝐶))) |
91 | | fvex 6113 |
. . . . . . . . . 10
⊢
(1st ‘𝑦) ∈ V |
92 | | fvex 6113 |
. . . . . . . . . 10
⊢ ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑦)) ∈ V |
93 | 91, 92 | opth 4871 |
. . . . . . . . 9
⊢
(〈(1st ‘𝑦), ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦))〉 =
〈(1st ‘𝑧), ((𝑓‘(1st ‘𝑧))‘(2nd
‘𝑧))〉 ↔
((1st ‘𝑦)
= (1st ‘𝑧)
∧ ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧)))) |
94 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (1st
‘𝑦) = (1st
‘𝑧)) |
95 | 94 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (𝑓‘(1st ‘𝑦)) = (𝑓‘(1st ‘𝑧))) |
96 | 95 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑧)) = ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧))) |
97 | 96 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑧)) ↔ ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧)))) |
98 | | djussxp 5189 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V) |
99 | 66, 98 | eqsstri 3598 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑇 ⊆ (𝐴 × V) |
100 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑦 ∈ 𝑇) |
101 | 99, 100 | sseldi 3566 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑦 ∈ (𝐴 × V)) |
102 | 101 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → 𝑦 ∈ (𝐴 × V)) |
103 | | xp1st 7089 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (𝐴 × V) → (1st
‘𝑦) ∈ 𝐴) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (1st
‘𝑦) ∈ 𝐴) |
105 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶) |
106 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑓‘(1st ‘𝑦)) |
107 | | nfcsb1v 3515 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥⦋(1st ‘𝑦) / 𝑥⦌𝐵 |
108 | 106, 107,
27 | nff1 6012 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑓‘(1st
‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶 |
109 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (1st ‘𝑦) → (𝑓‘𝑥) = (𝑓‘(1st ‘𝑦))) |
110 | | f1eq1 6009 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓‘𝑥) = (𝑓‘(1st ‘𝑦)) → ((𝑓‘𝑥):𝐵–1-1→𝐶 ↔ (𝑓‘(1st ‘𝑦)):𝐵–1-1→𝐶)) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (1st ‘𝑦) → ((𝑓‘𝑥):𝐵–1-1→𝐶 ↔ (𝑓‘(1st ‘𝑦)):𝐵–1-1→𝐶)) |
112 | | csbeq1a 3508 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (1st ‘𝑦) → 𝐵 = ⦋(1st
‘𝑦) / 𝑥⦌𝐵) |
113 | | f1eq2 6010 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 =
⦋(1st ‘𝑦) / 𝑥⦌𝐵 → ((𝑓‘(1st ‘𝑦)):𝐵–1-1→𝐶 ↔ (𝑓‘(1st ‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶)) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (1st ‘𝑦) → ((𝑓‘(1st ‘𝑦)):𝐵–1-1→𝐶 ↔ (𝑓‘(1st ‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶)) |
115 | 111, 114 | bitrd 267 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (1st ‘𝑦) → ((𝑓‘𝑥):𝐵–1-1→𝐶 ↔ (𝑓‘(1st ‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶)) |
116 | 108, 115 | rspc 3276 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑦) ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → (𝑓‘(1st ‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶)) |
117 | 104, 105,
116 | sylc 63 |
. . . . . . . . . . . . 13
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (𝑓‘(1st ‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶) |
118 | 107 | nfel2 2767 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(2nd ‘𝑦) ∈ ⦋(1st
‘𝑦) / 𝑥⦌𝐵 |
119 | 74 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥 = (1st ‘𝑦)) |
120 | 119, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → 𝐵 = ⦋(1st
‘𝑦) / 𝑥⦌𝐵) |
121 | 82, 120 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ 𝐴 ∧ ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵))) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
122 | 121 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐴 → (((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵)) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵)) |
123 | 118, 122 | rexlimi 3006 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑥 ∈
𝐴 ((𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ ({𝑥} × 𝐵)) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
124 | 70, 123 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ ∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
125 | 124 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → (∃𝑥 ∈ 𝐴 𝑦 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵)) |
126 | 69, 125 | syl5bi 231 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → (𝑦 ∈ 𝑇 → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵)) |
127 | 126 | imp 444 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑦 ∈ 𝑇) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
128 | 127 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
129 | 128 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (2nd
‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
130 | 126 | ralrimiv 2948 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → ∀𝑦 ∈ 𝑇 (2nd ‘𝑦) ∈ ⦋(1st
‘𝑦) / 𝑥⦌𝐵) |
131 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑧 → (2nd ‘𝑦) = (2nd ‘𝑧)) |
132 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑧 → (1st ‘𝑦) = (1st ‘𝑧)) |
133 | 132 | csbeq1d 3506 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑧 → ⦋(1st
‘𝑦) / 𝑥⦌𝐵 = ⦋(1st
‘𝑧) / 𝑥⦌𝐵) |
134 | 131, 133 | eleq12d 2682 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑧 → ((2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵 ↔ (2nd ‘𝑧) ∈
⦋(1st ‘𝑧) / 𝑥⦌𝐵)) |
135 | 134 | rspccva 3281 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑦 ∈
𝑇 (2nd
‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵 ∧ 𝑧 ∈ 𝑇) → (2nd ‘𝑧) ∈
⦋(1st ‘𝑧) / 𝑥⦌𝐵) |
136 | 130, 135 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ 𝑧 ∈ 𝑇) → (2nd ‘𝑧) ∈
⦋(1st ‘𝑧) / 𝑥⦌𝐵) |
137 | 136 | adantrl 748 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (2nd ‘𝑧) ∈
⦋(1st ‘𝑧) / 𝑥⦌𝐵) |
138 | 137 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (2nd
‘𝑧) ∈
⦋(1st ‘𝑧) / 𝑥⦌𝐵) |
139 | 94 | csbeq1d 3506 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) →
⦋(1st ‘𝑦) / 𝑥⦌𝐵 = ⦋(1st
‘𝑧) / 𝑥⦌𝐵) |
140 | 138, 139 | eleqtrrd 2691 |
. . . . . . . . . . . . 13
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (2nd
‘𝑧) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵) |
141 | | f1fveq 6420 |
. . . . . . . . . . . . 13
⊢ (((𝑓‘(1st
‘𝑦)):⦋(1st
‘𝑦) / 𝑥⦌𝐵–1-1→𝐶 ∧ ((2nd ‘𝑦) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵 ∧ (2nd ‘𝑧) ∈
⦋(1st ‘𝑦) / 𝑥⦌𝐵)) → (((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑧)) ↔ (2nd
‘𝑦) = (2nd
‘𝑧))) |
142 | 117, 129,
140, 141 | syl12anc 1316 |
. . . . . . . . . . . 12
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑧)) ↔ (2nd
‘𝑦) = (2nd
‘𝑧))) |
143 | 97, 142 | bitr3d 269 |
. . . . . . . . . . 11
⊢
(((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) ∧ (1st ‘𝑦) = (1st ‘𝑧)) → (((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧)) ↔ (2nd
‘𝑦) = (2nd
‘𝑧))) |
144 | 143 | pm5.32da 671 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((1st ‘𝑦) = (1st ‘𝑧) ∧ ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧))) ↔ ((1st
‘𝑦) = (1st
‘𝑧) ∧
(2nd ‘𝑦) =
(2nd ‘𝑧)))) |
145 | | simprr 792 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑧 ∈ 𝑇) |
146 | 99, 145 | sseldi 3566 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → 𝑧 ∈ (𝐴 × V)) |
147 | | xpopth 7098 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ (𝐴 × V) ∧ 𝑧 ∈ (𝐴 × V)) → (((1st
‘𝑦) = (1st
‘𝑧) ∧
(2nd ‘𝑦) =
(2nd ‘𝑧))
↔ 𝑦 = 𝑧)) |
148 | 101, 146,
147 | syl2anc 691 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((1st ‘𝑦) = (1st ‘𝑧) ∧ (2nd
‘𝑦) = (2nd
‘𝑧)) ↔ 𝑦 = 𝑧)) |
149 | 144, 148 | bitrd 267 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (((1st ‘𝑦) = (1st ‘𝑧) ∧ ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦)) = ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧))) ↔ 𝑦 = 𝑧)) |
150 | 93, 149 | syl5bb 271 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 ∧ (𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇)) → (〈(1st
‘𝑦), ((𝑓‘(1st
‘𝑦))‘(2nd ‘𝑦))〉 = 〈(1st
‘𝑧), ((𝑓‘(1st
‘𝑧))‘(2nd ‘𝑧))〉 ↔ 𝑦 = 𝑧)) |
151 | 150 | ex 449 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → ((𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → (〈(1st ‘𝑦), ((𝑓‘(1st ‘𝑦))‘(2nd
‘𝑦))〉 =
〈(1st ‘𝑧), ((𝑓‘(1st ‘𝑧))‘(2nd
‘𝑧))〉 ↔
𝑦 = 𝑧))) |
152 | 90, 151 | dom2d 7882 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → ((𝐴 × 𝐶) ∈ V → 𝑇 ≼ (𝐴 × 𝐶))) |
153 | 65, 152 | syl5com 31 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥):𝐵–1-1→𝐶 → 𝑇 ≼ (𝐴 × 𝐶))) |
154 | 48, 153 | syl5bir 232 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ 𝐴 (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶 → 𝑇 ≼ (𝐴 × 𝐶))) |
155 | 154 | adantld 482 |
. . 3
⊢ (𝜑 → ((𝑓:𝐴⟶∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵) ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶) → 𝑇 ≼ (𝐴 × 𝐶))) |
156 | 155 | exlimdv 1848 |
. 2
⊢ (𝜑 → (∃𝑓(𝑓:𝐴⟶∪
𝑥 ∈ 𝐴 (𝐶 ↑𝑚 𝐵) ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦):⦋𝑦 / 𝑥⦌𝐵–1-1→𝐶) → 𝑇 ≼ (𝐴 × 𝐶))) |
157 | 38, 156 | mpd 15 |
1
⊢ (𝜑 → 𝑇 ≼ (𝐴 × 𝐶)) |