MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iundom2g Structured version   Visualization version   GIF version

Theorem iundom2g 10181
Description: An upper bound for the cardinality of a disjoint indexed union, with explicit choice principles. 𝐵 depends on 𝑥 and should be thought of as 𝐵(𝑥). (Contributed by Mario Carneiro, 1-Sep-2015.)
Hypotheses
Ref Expression
iunfo.1 𝑇 = 𝑥𝐴 ({𝑥} × 𝐵)
iundomg.2 (𝜑 𝑥𝐴 (𝐶m 𝐵) ∈ AC 𝐴)
iundomg.3 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
Assertion
Ref Expression
iundom2g (𝜑𝑇 ≼ (𝐴 × 𝐶))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑇(𝑥)

Proof of Theorem iundom2g
Dummy variables 𝑓 𝑔 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iundomg.2 . . 3 (𝜑 𝑥𝐴 (𝐶m 𝐵) ∈ AC 𝐴)
2 iundomg.3 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
3 brdomi 8662 . . . . . . . . 9 (𝐵𝐶 → ∃𝑔 𝑔:𝐵1-1𝐶)
43adantl 485 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → ∃𝑔 𝑔:𝐵1-1𝐶)
5 f1f 6636 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐶𝑔:𝐵𝐶)
6 reldom 8655 . . . . . . . . . . . . . . 15 Rel ≼
76brrelex2i 5623 . . . . . . . . . . . . . 14 (𝐵𝐶𝐶 ∈ V)
86brrelex1i 5622 . . . . . . . . . . . . . 14 (𝐵𝐶𝐵 ∈ V)
97, 8elmapd 8545 . . . . . . . . . . . . 13 (𝐵𝐶 → (𝑔 ∈ (𝐶m 𝐵) ↔ 𝑔:𝐵𝐶))
109adantl 485 . . . . . . . . . . . 12 ((𝑥𝐴𝐵𝐶) → (𝑔 ∈ (𝐶m 𝐵) ↔ 𝑔:𝐵𝐶))
115, 10syl5ibr 249 . . . . . . . . . . 11 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶𝑔 ∈ (𝐶m 𝐵)))
12 ssiun2 4972 . . . . . . . . . . . . 13 (𝑥𝐴 → (𝐶m 𝐵) ⊆ 𝑥𝐴 (𝐶m 𝐵))
1312adantr 484 . . . . . . . . . . . 12 ((𝑥𝐴𝐵𝐶) → (𝐶m 𝐵) ⊆ 𝑥𝐴 (𝐶m 𝐵))
1413sseld 3916 . . . . . . . . . . 11 ((𝑥𝐴𝐵𝐶) → (𝑔 ∈ (𝐶m 𝐵) → 𝑔 𝑥𝐴 (𝐶m 𝐵)))
1511, 14syld 47 . . . . . . . . . 10 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶𝑔 𝑥𝐴 (𝐶m 𝐵)))
1615ancrd 555 . . . . . . . . 9 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶 → (𝑔 𝑥𝐴 (𝐶m 𝐵) ∧ 𝑔:𝐵1-1𝐶)))
1716eximdv 1925 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → (∃𝑔 𝑔:𝐵1-1𝐶 → ∃𝑔(𝑔 𝑥𝐴 (𝐶m 𝐵) ∧ 𝑔:𝐵1-1𝐶)))
184, 17mpd 15 . . . . . . 7 ((𝑥𝐴𝐵𝐶) → ∃𝑔(𝑔 𝑥𝐴 (𝐶m 𝐵) ∧ 𝑔:𝐵1-1𝐶))
19 df-rex 3069 . . . . . . 7 (∃𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶 ↔ ∃𝑔(𝑔 𝑥𝐴 (𝐶m 𝐵) ∧ 𝑔:𝐵1-1𝐶))
2018, 19sylibr 237 . . . . . 6 ((𝑥𝐴𝐵𝐶) → ∃𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶)
2120ralimiaa 3085 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶)
222, 21syl 17 . . . 4 (𝜑 → ∀𝑥𝐴𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶)
23 nfv 1922 . . . . 5 𝑦𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶
24 nfiu1 4954 . . . . . 6 𝑥 𝑥𝐴 (𝐶m 𝐵)
25 nfcv 2906 . . . . . . 7 𝑥𝑔
26 nfcsb1v 3852 . . . . . . 7 𝑥𝑦 / 𝑥𝐵
27 nfcv 2906 . . . . . . 7 𝑥𝐶
2825, 26, 27nff1 6634 . . . . . 6 𝑥 𝑔:𝑦 / 𝑥𝐵1-1𝐶
2924, 28nfrex 3237 . . . . 5 𝑥𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶
30 csbeq1a 3841 . . . . . . 7 (𝑥 = 𝑦𝐵 = 𝑦 / 𝑥𝐵)
31 f1eq2 6632 . . . . . . 7 (𝐵 = 𝑦 / 𝑥𝐵 → (𝑔:𝐵1-1𝐶𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3230, 31syl 17 . . . . . 6 (𝑥 = 𝑦 → (𝑔:𝐵1-1𝐶𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3332rexbidv 3225 . . . . 5 (𝑥 = 𝑦 → (∃𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶 ↔ ∃𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3423, 29, 33cbvralw 3363 . . . 4 (∀𝑥𝐴𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶 ↔ ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶)
3522, 34sylib 221 . . 3 (𝜑 → ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶)
36 f1eq1 6631 . . . 4 (𝑔 = (𝑓𝑦) → (𝑔:𝑦 / 𝑥𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
3736acni3 9688 . . 3 (( 𝑥𝐴 (𝐶m 𝐵) ∈ AC 𝐴 ∧ ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶) → ∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶m 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
381, 35, 37syl2anc 587 . 2 (𝜑 → ∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶m 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
39 nfv 1922 . . . . . 6 𝑦(𝑓𝑥):𝐵1-1𝐶
40 nfcv 2906 . . . . . . 7 𝑥(𝑓𝑦)
4140, 26, 27nff1 6634 . . . . . 6 𝑥(𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶
42 fveq2 6738 . . . . . . . 8 (𝑥 = 𝑦 → (𝑓𝑥) = (𝑓𝑦))
43 f1eq1 6631 . . . . . . . 8 ((𝑓𝑥) = (𝑓𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝐵1-1𝐶))
4442, 43syl 17 . . . . . . 7 (𝑥 = 𝑦 → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝐵1-1𝐶))
45 f1eq2 6632 . . . . . . . 8 (𝐵 = 𝑦 / 𝑥𝐵 → ((𝑓𝑦):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4630, 45syl 17 . . . . . . 7 (𝑥 = 𝑦 → ((𝑓𝑦):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4744, 46bitrd 282 . . . . . 6 (𝑥 = 𝑦 → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4839, 41, 47cbvralw 3363 . . . . 5 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ↔ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶)
49 df-ne 2943 . . . . . . . 8 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
50 acnrcl 9683 . . . . . . . . . 10 ( 𝑥𝐴 (𝐶m 𝐵) ∈ AC 𝐴𝐴 ∈ V)
511, 50syl 17 . . . . . . . . 9 (𝜑𝐴 ∈ V)
52 r19.2z 4422 . . . . . . . . . . . 12 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝐵𝐶) → ∃𝑥𝐴 𝐵𝐶)
537rexlimivw 3210 . . . . . . . . . . . 12 (∃𝑥𝐴 𝐵𝐶𝐶 ∈ V)
5452, 53syl 17 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝐵𝐶) → 𝐶 ∈ V)
5554expcom 417 . . . . . . . . . 10 (∀𝑥𝐴 𝐵𝐶 → (𝐴 ≠ ∅ → 𝐶 ∈ V))
562, 55syl 17 . . . . . . . . 9 (𝜑 → (𝐴 ≠ ∅ → 𝐶 ∈ V))
57 xpexg 7556 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 × 𝐶) ∈ V)
5851, 56, 57syl6an 684 . . . . . . . 8 (𝜑 → (𝐴 ≠ ∅ → (𝐴 × 𝐶) ∈ V))
5949, 58syl5bir 246 . . . . . . 7 (𝜑 → (¬ 𝐴 = ∅ → (𝐴 × 𝐶) ∈ V))
60 xpeq1 5582 . . . . . . . 8 (𝐴 = ∅ → (𝐴 × 𝐶) = (∅ × 𝐶))
61 0xp 5663 . . . . . . . . 9 (∅ × 𝐶) = ∅
62 0ex 5216 . . . . . . . . 9 ∅ ∈ V
6361, 62eqeltri 2836 . . . . . . . 8 (∅ × 𝐶) ∈ V
6460, 63eqeltrdi 2848 . . . . . . 7 (𝐴 = ∅ → (𝐴 × 𝐶) ∈ V)
6559, 64pm2.61d2 184 . . . . . 6 (𝜑 → (𝐴 × 𝐶) ∈ V)
66 iunfo.1 . . . . . . . . . 10 𝑇 = 𝑥𝐴 ({𝑥} × 𝐵)
6766eleq2i 2831 . . . . . . . . 9 (𝑦𝑇𝑦 𝑥𝐴 ({𝑥} × 𝐵))
68 eliun 4924 . . . . . . . . 9 (𝑦 𝑥𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵))
6967, 68bitri 278 . . . . . . . 8 (𝑦𝑇 ↔ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵))
70 r19.29 3183 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → ∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)))
71 xp1st 7814 . . . . . . . . . . . . . . 15 (𝑦 ∈ ({𝑥} × 𝐵) → (1st𝑦) ∈ {𝑥})
7271ad2antll 729 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) ∈ {𝑥})
73 elsni 4574 . . . . . . . . . . . . . 14 ((1st𝑦) ∈ {𝑥} → (1st𝑦) = 𝑥)
7472, 73syl 17 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) = 𝑥)
75 simpl 486 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥𝐴)
7674, 75eqeltrd 2840 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) ∈ 𝐴)
7774fveq2d 6742 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓‘(1st𝑦)) = (𝑓𝑥))
7877fveq1d 6740 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓𝑥)‘(2nd𝑦)))
79 f1f 6636 . . . . . . . . . . . . . . 15 ((𝑓𝑥):𝐵1-1𝐶 → (𝑓𝑥):𝐵𝐶)
8079ad2antrl 728 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓𝑥):𝐵𝐶)
81 xp2nd 7815 . . . . . . . . . . . . . . 15 (𝑦 ∈ ({𝑥} × 𝐵) → (2nd𝑦) ∈ 𝐵)
8281ad2antll 729 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (2nd𝑦) ∈ 𝐵)
8380, 82ffvelrnd 6926 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓𝑥)‘(2nd𝑦)) ∈ 𝐶)
8478, 83eqeltrd 2840 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ 𝐶)
8576, 84opelxpd 5606 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8685rexlimiva 3209 . . . . . . . . . 10 (∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8770, 86syl 17 . . . . . . . . 9 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8887ex 416 . . . . . . . 8 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶)))
8969, 88syl5bi 245 . . . . . . 7 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑦𝑇 → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶)))
90 fvex 6751 . . . . . . . . . 10 (1st𝑦) ∈ V
91 fvex 6751 . . . . . . . . . 10 ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ V
9290, 91opth 5376 . . . . . . . . 9 (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ ((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))))
93 simpr 488 . . . . . . . . . . . . . . 15 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) = (1st𝑧))
9493fveq2d 6742 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (𝑓‘(1st𝑦)) = (𝑓‘(1st𝑧)))
9594fveq1d 6740 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → ((𝑓‘(1st𝑦))‘(2nd𝑧)) = ((𝑓‘(1st𝑧))‘(2nd𝑧)))
9695eqeq2d 2750 . . . . . . . . . . . 12 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))))
97 djussxp 5731 . . . . . . . . . . . . . . . . . 18 𝑥𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V)
9866, 97eqsstri 3951 . . . . . . . . . . . . . . . . 17 𝑇 ⊆ (𝐴 × V)
99 simprl 771 . . . . . . . . . . . . . . . . 17 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑦𝑇)
10098, 99sselid 3914 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑦 ∈ (𝐴 × V))
101100adantr 484 . . . . . . . . . . . . . . 15 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → 𝑦 ∈ (𝐴 × V))
102 xp1st 7814 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝐴 × V) → (1st𝑦) ∈ 𝐴)
103101, 102syl 17 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) ∈ 𝐴)
104 simpll 767 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → ∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶)
105 nfcv 2906 . . . . . . . . . . . . . . . 16 𝑥(𝑓‘(1st𝑦))
106 nfcsb1v 3852 . . . . . . . . . . . . . . . 16 𝑥(1st𝑦) / 𝑥𝐵
107105, 106, 27nff1 6634 . . . . . . . . . . . . . . 15 𝑥(𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶
108 fveq2 6738 . . . . . . . . . . . . . . . . 17 (𝑥 = (1st𝑦) → (𝑓𝑥) = (𝑓‘(1st𝑦)))
109 f1eq1 6631 . . . . . . . . . . . . . . . . 17 ((𝑓𝑥) = (𝑓‘(1st𝑦)) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):𝐵1-1𝐶))
110108, 109syl 17 . . . . . . . . . . . . . . . 16 (𝑥 = (1st𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):𝐵1-1𝐶))
111 csbeq1a 3841 . . . . . . . . . . . . . . . . 17 (𝑥 = (1st𝑦) → 𝐵 = (1st𝑦) / 𝑥𝐵)
112 f1eq2 6632 . . . . . . . . . . . . . . . . 17 (𝐵 = (1st𝑦) / 𝑥𝐵 → ((𝑓‘(1st𝑦)):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
113111, 112syl 17 . . . . . . . . . . . . . . . 16 (𝑥 = (1st𝑦) → ((𝑓‘(1st𝑦)):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
114110, 113bitrd 282 . . . . . . . . . . . . . . 15 (𝑥 = (1st𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
115107, 114rspc 3539 . . . . . . . . . . . . . 14 ((1st𝑦) ∈ 𝐴 → (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
116103, 104, 115sylc 65 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶)
117106nfel2 2924 . . . . . . . . . . . . . . . . . . . 20 𝑥(2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵
11874eqcomd 2745 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥 = (1st𝑦))
119118, 111syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝐵 = (1st𝑦) / 𝑥𝐵)
12082, 119eleqtrd 2842 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
121120ex 416 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐴 → (((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
122117, 121rexlimi 3243 . . . . . . . . . . . . . . . . . . 19 (∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
12370, 122syl 17 . . . . . . . . . . . . . . . . . 18 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
124123ex 416 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
12569, 124syl5bi 245 . . . . . . . . . . . . . . . 16 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑦𝑇 → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
126125imp 410 . . . . . . . . . . . . . . 15 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑦𝑇) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
127126adantrr 717 . . . . . . . . . . . . . 14 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
128127adantr 484 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
129125ralrimiv 3106 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ∀𝑦𝑇 (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
130 fveq2 6738 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (2nd𝑦) = (2nd𝑧))
131 fveq2 6738 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑧 → (1st𝑦) = (1st𝑧))
132131csbeq1d 3831 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧(1st𝑦) / 𝑥𝐵 = (1st𝑧) / 𝑥𝐵)
133130, 132eleq12d 2834 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵 ↔ (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵))
134133rspccva 3550 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝑇 (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵𝑧𝑇) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
135129, 134sylan 583 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑧𝑇) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
136135adantrl 716 . . . . . . . . . . . . . . 15 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
137136adantr 484 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
13893csbeq1d 3831 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) / 𝑥𝐵 = (1st𝑧) / 𝑥𝐵)
139137, 138eleqtrrd 2843 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑧) ∈ (1st𝑦) / 𝑥𝐵)
140 f1fveq 7095 . . . . . . . . . . . . 13 (((𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶 ∧ ((2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵 ∧ (2nd𝑧) ∈ (1st𝑦) / 𝑥𝐵)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
141116, 128, 139, 140syl12anc 837 . . . . . . . . . . . 12 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
14296, 141bitr3d 284 . . . . . . . . . . 11 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
143142pm5.32da 582 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))) ↔ ((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧))))
144 simprr 773 . . . . . . . . . . . 12 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑧𝑇)
14598, 144sselid 3914 . . . . . . . . . . 11 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑧 ∈ (𝐴 × V))
146 xpopth 7823 . . . . . . . . . . 11 ((𝑦 ∈ (𝐴 × V) ∧ 𝑧 ∈ (𝐴 × V)) → (((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧)) ↔ 𝑦 = 𝑧))
147100, 145, 146syl2anc 587 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧)) ↔ 𝑦 = 𝑧))
148143, 147bitrd 282 . . . . . . . . 9 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))) ↔ 𝑦 = 𝑧))
14992, 148syl5bb 286 . . . . . . . 8 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ 𝑦 = 𝑧))
150149ex 416 . . . . . . 7 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ((𝑦𝑇𝑧𝑇) → (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ 𝑦 = 𝑧)))
15189, 150dom2d 8694 . . . . . 6 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ((𝐴 × 𝐶) ∈ V → 𝑇 ≼ (𝐴 × 𝐶)))
15265, 151syl5com 31 . . . . 5 (𝜑 → (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑇 ≼ (𝐴 × 𝐶)))
15348, 152syl5bir 246 . . . 4 (𝜑 → (∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶𝑇 ≼ (𝐴 × 𝐶)))
154153adantld 494 . . 3 (𝜑 → ((𝑓:𝐴 𝑥𝐴 (𝐶m 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶) → 𝑇 ≼ (𝐴 × 𝐶)))
155154exlimdv 1941 . 2 (𝜑 → (∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶m 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶) → 𝑇 ≼ (𝐴 × 𝐶)))
15638, 155mpd 15 1 (𝜑𝑇 ≼ (𝐴 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1543  wex 1787  wcel 2112  wne 2942  wral 3063  wrex 3064  Vcvv 3422  csb 3827  wss 3882  c0 4253  {csn 4557  cop 4563   ciun 4920   class class class wbr 5069   × cxp 5566  wf 6396  1-1wf1 6397  cfv 6400  (class class class)co 7234  1st c1st 7780  2nd c2nd 7781  m cmap 8531  cdom 8647  AC wacn 9581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5195  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3711  df-csb 3828  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-id 5471  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-ov 7237  df-oprab 7238  df-mpo 7239  df-1st 7782  df-2nd 7783  df-map 8533  df-dom 8651  df-acn 9585
This theorem is referenced by:  iundomg  10182  iundom  10183
  Copyright terms: Public domain W3C validator