Theorem ssrel

Description: A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of Monk1 p. 33. (Contributed by NM, 2-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021) Remove dependency on ax-12 . (Revised by SN, 11-Dec-2024)

	Ref	Expression
Assertion	ssrel	⊢ ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssel	⊢ ( 𝐴 ⊆ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
2	1	alrimivv	⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
3		df-rel	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
4		df-ss	⊢ ( 𝐴 ⊆ ( V × V ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( V × V ) ) )
5	3 4	sylbb	⊢ ( Rel 𝐴 → ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( V × V ) ) )
6		elopabw	⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) ) )
7	6	elv	⊢ ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) )
8		simpl	⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
9	8	2eximi	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
10	7 9	sylbi	⊢ ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
11		df-xp	⊢ ( V × V ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
12	10 11	eleq2s	⊢ ( 𝑧 ∈ ( V × V ) → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
13	12	imim2i	⊢ ( ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( V × V ) ) → ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
14	5 13	sylg	⊢ ( Rel 𝐴 → ∀ 𝑧 ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) )
15		eleq1	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
16		eleq1	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐵 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
17	15 16	imbi12d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
18	17	biimprcd	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
19	18	2alimi	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ∀ 𝑥 ∀ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
20		19.23vv	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
21	19 20	sylib	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
22	21	com23	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( 𝑧 ∈ 𝐴 → ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 ∈ 𝐵 ) ) )
23	22	a2d	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
24	23	alimdv	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
25	14 24	syl5	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( Rel 𝐴 → ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
26		df-ss	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) )
27	25 26	imbitrrdi	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( Rel 𝐴 → 𝐴 ⊆ 𝐵 ) )
28	27	com12	⊢ ( Rel 𝐴 → ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → 𝐴 ⊆ 𝐵 ) )
29	2 28	impbid2	⊢ ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )